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