let Al be QC-alphabet ; :: thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= VERUM Al iff CX |- VERUM Al )
let CX be Consistent Subset of (CQC-WFF Al); :: thesis: for JH being Henkin_interpretation of CX holds
( JH, valH Al |= VERUM Al iff CX |- VERUM Al )
let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH Al |= VERUM Al iff CX |- VERUM Al )
set f = <*> (CQC-WFF Al);
( rng (<*> (CQC-WFF Al)) c= CX & |- (<*> (CQC-WFF Al)) ^ <*(VERUM Al)*> ) by Th15;
hence ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) by VALUAT_1:32; :: thesis: verum