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