environ given s being STATEMENT; == No other premises. begin 1: now assume step1: not (True[s] or not True[s]); step2: now assume step3: not True[s]; step4: True[s] or not True[s] by step3; == DI thus step5: contradiction by step1, step4; == ContrI end; step6: True[s] by step2; == PbyC step7: True[s] or not True[s] by step6; == DI thus contradiction by step1, step7 == ContrI end; True[s] or not True[s] by 1 == PbyC