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