let CX be Consistent Subset of CQC-WFF ; :: thesis: for JH being Henkin_interpretation of CX holds
( JH, valH |= VERUM iff CX |- VERUM )
let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH |= VERUM iff CX |- VERUM )
set f = <*> CQC-WFF ;
( rng (<*> CQC-WFF ) c= CX & |- (<*> CQC-WFF ) ^ <*VERUM *> ) by Th15, RELAT_1:60, XBOOLE_1:2;
hence ( JH, valH |= VERUM iff CX |- VERUM ) by Def2, VALUAT_1:44; :: thesis: verum