let PHI be Subset of (CQC-WFF Al); :: thesis: ( PHI is Consistent implies PHI is satisfiable )
assume A1: PHI is Consistent ; :: thesis: PHI is satisfiable
then consider Al2 being Al -expanding QC-alphabet , PSI being Consistent Subset of (CQC-WFF Al2) such that
A2: ( PHI c= PSI & PSI is with_examples ) by Th10;
consider THETA being Consistent Subset of (CQC-WFF Al2) such that
A3: ( THETA is negation_faithful & PSI c= THETA ) by Th12;
set JH = the Henkin_interpretation of THETA;
now :: thesis: for p being Element of CQC-WFF Al2 st p in THETA holds
the Henkin_interpretation of THETA, valH Al2 |= p
let p be Element of CQC-WFF Al2; :: thesis: ( p in THETA implies the Henkin_interpretation of THETA, valH Al2 |= p )
A4: THETA is with_examples by Th13, A3, A2;
assume p in THETA ; :: thesis: the Henkin_interpretation of THETA, valH Al2 |= p
then THETA |- p by GOEDELCP:21;
hence the Henkin_interpretation of THETA, valH Al2 |= p by GOEDELCP:17, A3, A4; :: thesis: verum
end;
then the Henkin_interpretation of THETA, valH Al2 |= THETA by CALCUL_1:def 11;
then ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI by A1, A2, A3, QC_TRANS:10, XBOOLE_1:1;
hence PHI is satisfiable ; :: thesis: verum