let p be Element of CQC-WFF ; :: thesis: ( p in TAUT iff 'not' ('not' p) in TAUT )
thus ( p in TAUT implies 'not' ('not' p) in TAUT ) :: thesis: ( 'not' ('not' p) in TAUT implies p in TAUT )

proof

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

end;

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