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