let A be QC-alphabet ; :: thesis: ( VERUM A is closed & FALSUM A is closed )
( still_not-bound_in (VERUM A) = {} & still_not-bound_in (FALSUM A) = {} ) by Th3, Th8;
hence ( VERUM A is closed & FALSUM A is closed ) by QC_LANG1:def 31; :: thesis: verum