let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p <=> q is valid holds
( p is valid iff q is valid )
let p, q be Element of CQC-WFF A; :: thesis: ( p <=> q is valid implies ( p is valid iff q is valid ) )
assume A1: p <=> q in TAUT A ; :: according to CQC_THE1:def 10 :: thesis: ( p is valid iff q is valid )
(p <=> q) => (p => q) in TAUT A by PROCAL_1:23;
then A2: p => q in TAUT A by A1, CQC_THE1:46;
thus ( p is valid implies q is valid ) by A2, CQC_THE1:46; :: thesis: ( q is valid implies p is valid )
assume A3: q in TAUT A ; :: according to CQC_THE1:def 10 :: thesis: p is valid
(p <=> q) => (q => p) in TAUT A by PROCAL_1:24;
then q => p in TAUT A by A1, CQC_THE1:46;
hence p in TAUT A by A3, CQC_THE1:46; :: according to CQC_THE1:def 10 :: thesis: verum