let Al be QC-alphabet ; :: thesis: for PSI being Consistent Subset of (CQC-WFF Al) ex THETA being Consistent Subset of (CQC-WFF Al) st
( THETA is negation_faithful & PSI c= THETA )

let PSI be Consistent Subset of (CQC-WFF Al); :: thesis: ex THETA being Consistent Subset of (CQC-WFF Al) st
( THETA is negation_faithful & PSI c= THETA )

set U = { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } ;
A1: PSI in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } ;
for Z being set st Z c= { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & Z is c=-linear holds
ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) )
proof
let Z be set ; :: thesis: ( Z c= { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & Z is c=-linear implies ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) ) )

assume A2: ( Z c= { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & Z is c=-linear ) ; :: thesis: ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) )

per cases ( Z is empty or not Z is empty ) ;
suppose A3: Z is empty ; :: thesis: ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) )

( PSI in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= PSI ) ) by A3;
hence ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) ) ; :: thesis: verum
end;
suppose A4: not Z is empty ; :: thesis: ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) )

set Y = union Z;
A5: PSI c= union Z
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in PSI or z in union Z )
assume A6: z in PSI ; :: thesis: z in union Z
consider X being object such that
A7: X in Z by ;
X in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } by A2, A7;
then ex R being Consistent Subset of (CQC-WFF Al) st
( X = R & PSI c= R ) ;
hence z in union Z by ; :: thesis: verum
end;
A8: union Z is Consistent Subset of (CQC-WFF Al)
proof
for X being set st X in Z holds
X c= CQC-WFF Al
proof
let X be set ; :: thesis: ( X in Z implies X c= CQC-WFF Al )
assume A9: X in Z ; :: thesis: X c= CQC-WFF Al
X in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } by A2, A9;
then ex R being Consistent Subset of (CQC-WFF Al) st
( X = R & PSI c= R ) ;
hence X c= CQC-WFF Al ; :: thesis: verum
end;
then reconsider Y = union Z as Subset of (CQC-WFF Al) by ZFMISC_1:76;
Y is Consistent
proof
assume Y is Inconsistent ; :: thesis: contradiction
then consider X being Subset of (CQC-WFF Al) such that
A10: ( X c= Y & X is finite & X is Inconsistent ) by HENMODEL:7;
ex Rs being finite Subset of Z st
for x being set st x in X holds
ex R being set st
( R in Rs & x in R )
proof
defpred S1[ set ] means ex Rs being finite Subset of Z st
for x being set st x in \$1 holds
ex R being set st
( R in Rs & x in R );
A11: S1[ {} ]
proof
consider Rs being object such that
A12: Rs in Z by ;
reconsider Rss = {Rs} as finite Subset of Z by ;
for x being set st x in {} holds
ex R being set st
( R in Rss & x in R ) ;
hence S1[ {} ] ; :: thesis: verum
end;
A13: for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume A14: ( x in X & B c= X & S1[B] ) ; :: thesis: S1[B \/ {x}]
consider Rs being finite Subset of Z such that
A15: for b being set st b in B holds
ex R being set st
( R in Rs & b in R ) by A14;
consider S being set such that
A16: ( x in S & S in Z ) by ;
set Rss = Rs \/ {S};
( Rs c= Z & {S} c= Z ) by ;
then A17: Rs \/ {S} c= Z by XBOOLE_1:8;
for y being set st y in B \/ {x} holds
ex R being set st
( R in Rs \/ {S} & y in R )
proof
let y be set ; :: thesis: ( y in B \/ {x} implies ex R being set st
( R in Rs \/ {S} & y in R ) )

assume A18: y in B \/ {x} ; :: thesis: ex R being set st
( R in Rs \/ {S} & y in R )

per cases ( y in {x} or y in B ) by ;
suppose y in {x} ; :: thesis: ex R being set st
( R in Rs \/ {S} & y in R )

end;
suppose y in B ; :: thesis: ex R being set st
( R in Rs \/ {S} & y in R )

then consider R being set such that
A20: ( R in Rs & y in R ) by A15;
R in Rs \/ {S} by ;
hence ex R being set st
( R in Rs \/ {S} & y in R ) by A20; :: thesis: verum
end;
end;
end;
hence S1[B \/ {x}] by A17; :: thesis: verum
end;
A21: X is finite by A10;
S1[X] from FINSET_1:sch 2(A21, A11, A13);
hence ex Rs being finite Subset of Z st
for x being set st x in X holds
ex R being set st
( R in Rs & x in R ) ; :: thesis: verum
end;
then consider Rs being finite Subset of Z such that
A22: for x being set st x in X holds
ex R being set st
( R in Rs & x in R ) ;
defpred S1[ set ] means ( not \$1 is empty implies union \$1 in \$1 );
A23: Rs is finite ;
A24: S1[ {} ] ;
A25: for x, B being set st x in Rs & B c= Rs & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in Rs & B c= Rs & S1[B] implies S1[B \/ {x}] )
assume A26: ( x in Rs & B c= Rs & S1[B] ) ; :: thesis: S1[B \/ {x}]
per cases ( B is empty or not B is empty ) ;
suppose A29: not B is empty ; :: thesis: S1[B \/ {x}]
per cases ( x c= union B or union B c= x ) by ;
suppose A30: x c= union B ; :: thesis: S1[B \/ {x}]
union (B \/ {x}) = () \/ () by ZFMISC_1:78
.= () \/ x by ZFMISC_1:25
.= union B by ;
hence S1[B \/ {x}] by ; :: thesis: verum
end;
suppose A31: union B c= x ; :: thesis: S1[B \/ {x}]
A32: x in {x} by TARSKI:def 1;
union (B \/ {x}) = () \/ () by ZFMISC_1:78
.= () \/ x by ZFMISC_1:25
.= x by ;
hence S1[B \/ {x}] by ; :: thesis: verum
end;
end;
end;
end;
end;
A33: S1[Rs] from FINSET_1:sch 2(A23, A24, A25);
not X is empty then consider x being object such that
A35: x in X by XBOOLE_0:def 1;
ex R being set st
( R in Rs & x in R ) by ;
then union Rs in Z by A33;
then union Rs in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } by A2;
then consider uRs being Consistent Subset of (CQC-WFF Al) such that
A36: ( union Rs = uRs & PSI c= uRs ) ;
for x being object st x in X holds
x in uRs
proof
let x be object ; :: thesis: ( x in X implies x in uRs )
assume A37: x in X ; :: thesis: x in uRs
ex R being set st
( R in Rs & x in R ) by ;
hence x in uRs by ; :: thesis: verum
end;
then A38: X c= uRs ;
consider f being FinSequence of CQC-WFF Al such that
A39: ( rng f c= X & |- f ^ <*('not' (VERUM Al))*> ) by ;
rng f c= uRs by ;
hence contradiction by A39, HENMODEL:def 1, GOEDELCP:24; :: thesis: verum
end;
hence union Z is Consistent Subset of (CQC-WFF Al) ; :: thesis: verum
end;
( union Z in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= union Z ) ) by ;
hence ex Y being set st
( Y in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for X being set st X in Z holds
X c= Y ) ) ; :: thesis: verum
end;
end;
end;
then consider THETA being set such that
A40: ( THETA in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & ( for Z being set st Z in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } & Z <> THETA holds
not THETA c= Z ) ) by ;
A41: ex PHI being Consistent Subset of (CQC-WFF Al) st
( PHI = THETA & PSI c= PHI ) by A40;
then reconsider THETA = THETA as Consistent Subset of (CQC-WFF Al) ;
A42: for p being Element of CQC-WFF Al holds
( p in THETA or 'not' p in THETA )
proof
let p be Element of CQC-WFF Al; :: thesis: ( p in THETA or 'not' p in THETA )
per cases ( THETA \/ {p} is Consistent or THETA \/ {()} is Consistent ) by Th11;
suppose A43: THETA \/ {p} is Consistent ; :: thesis: ( p in THETA or 'not' p in THETA )
assume A44: not p in THETA ; :: thesis: 'not' p in THETA
p in {p} by TARSKI:def 1;
then A45: ( p in THETA \/ {p} & not p in THETA ) by ;
PSI c= THETA \/ {p} by ;
then THETA \/ {p} in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } by A43;
hence 'not' p in THETA by ; :: thesis: verum
end;
suppose A46: THETA \/ {()} is Consistent ; :: thesis: ( p in THETA or 'not' p in THETA )
'not' p in THETA
proof
assume A47: not 'not' p in THETA ; :: thesis: contradiction
'not' p in {()} by TARSKI:def 1;
then A48: ( 'not' p in THETA \/ {()} & not 'not' p in THETA ) by ;
PSI c= THETA \/ {()} by ;
then THETA \/ {()} in { PHI where PHI is Consistent Subset of (CQC-WFF Al) : PSI c= PHI } by A46;
hence contradiction by A40, A48, XBOOLE_1:10; :: thesis: verum
end;
hence ( p in THETA or 'not' p in THETA ) ; :: thesis: verum
end;
end;
end;
for p being Element of CQC-WFF Al holds
( THETA |- p or THETA |- 'not' p )
proof
let p be Element of CQC-WFF Al; :: thesis: ( THETA |- p or THETA |- 'not' p )
( p in THETA or 'not' p in THETA ) by A42;
hence ( THETA |- p or THETA |- 'not' p ) by GOEDELCP:21; :: thesis: verum
end;
then THETA is negation_faithful by GOEDELCP:def 1;
hence ex THETA being Consistent Subset of (CQC-WFF Al) st
( THETA is negation_faithful & PSI c= THETA ) by A41; :: thesis: verum