let p, q be QC-formula; :: thesis: ( ( p is closed & q is closed ) iff p <=> q is closed )
p <=> q = (p => q) '&' (q => p) by QC_LANG2:def 4;
then ( ( p <=> q is closed implies ( p => q is closed & q => p is closed ) ) & ( p => q is closed & q => p is closed implies p <=> q is closed ) & ( q => p is closed implies ( p is closed & q is closed ) ) & ( p is closed & q is closed implies q => p is closed ) & ( p => q is closed implies ( p is closed & q is closed ) ) & ( p is closed & q is closed implies p => q is closed ) ) by Th26, Th30;
hence ( ( p is closed & q is closed ) iff p <=> q is closed ) ; :: thesis: verum