let p, q be Element of CQC-WFF ; :: thesis: ( p <==> q implies 'not' p <==> 'not' q )
assume p <==> q ; :: thesis: 'not' p <==> 'not' q
then ( p => q is valid & q => p is valid ) by Th50;
then ( ('not' p) => ('not' q) is valid & ('not' q) => ('not' p) is valid ) by LUKASI_1:63;
hence 'not' p <==> 'not' q by Th50; :: thesis: verum