let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds
( p in TAUT A iff 'not' ('not' p) in TAUT A )
let p be Element of CQC-WFF A; :: thesis: ( p in TAUT A iff 'not' ('not' p) in TAUT A )
thus ( p in TAUT A implies 'not' ('not' p) in TAUT A ) :: thesis: ( 'not' ('not' p) in TAUT A implies p in TAUT A )

proof

assume A1: p in TAUT A ; :: thesis: 'not' ('not' p) in TAUT A
p => ('not' ('not' p)) in TAUT A by Th27;
hence 'not' ('not' p) in TAUT A by A1, CQC_THE1:46; :: thesis: verum

end;

assume A2: 'not' ('not' p) in TAUT A ; :: thesis: p in TAUT A
('not' ('not' p)) => p in TAUT A by Th25;
hence p in TAUT A by A2, CQC_THE1:46; :: thesis: verum