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;

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

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

then
the Henkin_interpretation of THETA, valH Al2 |= THETA
by CALCUL_1:def 11;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;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

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