let A be QC-alphabet ; :: thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p <=> q is closed )
let p, q be QC-formula of A; :: 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 iff ( p => q is closed & q => p is closed ) ) by Th22;
hence ( ( p is closed & q is closed ) iff p <=> q is closed ) by Th26; :: thesis: verum