let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st 'not' p <==> 'not' q holds
p <==> q
let p, q be Element of CQC-WFF A; :: thesis: ( 'not' p <==> 'not' q implies p <==> q )
assume A1: 'not' p <==> 'not' q ; :: thesis: p <==> q
then ('not' q) => ('not' p) is valid by Th50;
then A2: p => q is valid by LUKASI_1:52;
('not' p) => ('not' q) is valid by A1, Th50;
then q => p is valid by LUKASI_1:52;
hence p <==> q by A2, Th50; :: thesis: verum