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