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