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:38, XBOOLE_1:2;
hence ( JH, valH |= VERUM iff CX |- VERUM ) by Def2, VALUAT_1:32; :: thesis: verum