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 & (p <=> q) => (q => p) in TAUT ) by PROCAL_1:23, PROCAL_1:24;
then A2: ( p => q in TAUT & q => p 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 q in TAUT ; :: according to CQC_THE1:def 11 :: thesis: p is valid
hence p in TAUT by A2, CQC_THE1:82; :: according to CQC_THE1:def 11 :: thesis: verum