let X be Subset of CQC-WFF; :: thesis: X |- VERUM
set f = <*> CQC-WFF;
A1: rng (<*> CQC-WFF) c= X by XBOOLE_1:2;
|- (<*> CQC-WFF) ^ <*VERUM*> by HENMODEL:15;
hence X |- VERUM by A1, HENMODEL:def 2; :: thesis: verum