let p, q be Element of CQC-WFF ; :: thesis: ( p <=> q is valid implies ( p is valid iff q is valid ) )
assume A1: p <=> q in TAUT ; :: according to CQC_THE1:def 11 :: thesis: ( p is valid iff q is valid )
(p <=> q) => (p => q) in TAUT by PROCAL_1:23;
then A2: p => q in TAUT by A1, CQC_THE1:82;
thus ( p is valid implies q is valid ) :: thesis: ( q is valid implies p is valid )

proof

assume p in TAUT ; :: according to CQC_THE1:def 11 :: thesis: q is valid
hence q in TAUT by A2, CQC_THE1:82; :: according to CQC_THE1:def 11 :: thesis: verum

end;

assume A3: q in TAUT ; :: according to CQC_THE1:def 11 :: thesis: p is valid
(p <=> q) => (q => p) in TAUT by PROCAL_1:24;
then q => p in TAUT by A1, CQC_THE1:82;
hence p in TAUT by A3, CQC_THE1:82; :: according to CQC_THE1:def 11 :: thesis: verum