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 A4, XBOOLE_0:7;
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 A6, A7, TARSKI:def 4; :: 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 S₁[ 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: S₁[ {} ]

proof

consider Rs being object such that
A12: Rs in Z by A4, XBOOLE_0:7;
set Rss = {Rs};
reconsider Rss = {Rs} as finite Subset of Z by A12, ZFMISC_1:31;
for x being set st x in {} holds
ex R being set st
( R in Rss & x in R ) ;
hence S₁[ {} ] ; :: thesis: verum

end;

A13: for x, B being set st x in X & B c= X & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in X & B c= X & S₁[B] implies S₁[B \/ {x}] )
assume A14: ( x in X & B c= X & S₁[B] ) ; :: thesis: S₁[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 A10, A14, TARSKI:def 4;
set Rss = Rs \/ {S};
( Rs c= Z & {S} c= Z ) by A16, ZFMISC_1:31;
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 A18, XBOOLE_0:def 3;

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

then A19: y = x by TARSKI:def 1;
S in {S} by TARSKI:def 1;
then S in Rs \/ {S} by XBOOLE_0:def 3;
hence ex R being set st
( R in Rs \/ {S} & y in R ) by A16, A19; :: thesis: verum

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 A20, XBOOLE_0:def 3;
hence ex R being set st
( R in Rs \/ {S} & y in R ) by A20; :: thesis: verum

end;

end;

end;

hence S₁[B \/ {x}] by A17; :: thesis: verum

end;

A21: X is finite by A10;
S₁[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 S₁[ set ] means ( not $1 is empty implies union $1 in $1 );
A23: Rs is finite ;
A24: S₁[ {} ] ;
A25: for x, B being set st x in Rs & B c= Rs & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in Rs & B c= Rs & S₁[B] implies S₁[B \/ {x}] )
assume A26: ( x in Rs & B c= Rs & S₁[B] ) ; :: thesis: S₁[B \/ {x}]

per cases ( B is empty or not B is empty ) ;

suppose A27: B is empty ; :: thesis: S₁[B \/ {x}]

A28: union (B \/ {x}) = x by A27, ZFMISC_1:25;
thus S₁[B \/ {x}] by A27, A28, TARSKI:def 1; :: thesis: verum

end;

suppose A29: not B is empty ; :: thesis: S₁[B \/ {x}]

per cases ( x c= union B or union B c= x ) by A2, A26, A29, ORDINAL1:def 8, XBOOLE_0:def 9;

suppose A30: x c= union B ; :: thesis: S₁[B \/ {x}]

union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25
.= union B by A30, XBOOLE_1:12 ;
hence S₁[B \/ {x}] by A26, A29, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A31: union B c= x ; :: thesis: S₁[B \/ {x}]

A32: x in {x} by TARSKI:def 1;
union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25
.= x by A31, XBOOLE_1:12 ;
hence S₁[B \/ {x}] by A32, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

A33: S₁[Rs] from FINSET_1:sch 2(A23, A24, A25);
not X is empty

proof

assume A34: X is empty ; :: thesis: contradiction
X |- 'not' (VERUM Al) by A10, HENMODEL:6;
then ( X \/ {(VERUM Al)} is Inconsistent & X \/ {(VERUM Al)} = {(VERUM Al)} ) by A34, HENMODEL:10;
hence contradiction by HENMODEL:13; :: thesis: verum

end;

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 A22, A35;
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 A22, A37;
hence x in uRs by A36, TARSKI:def 4; :: 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 A10, HENMODEL:def 1, GOEDELCP:24;
rng f c= uRs by A38, A39;
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 A5, A8, ZFMISC_1:74;
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 A1, ORDERS_1:65;
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 \/ {('not' p)} 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 XBOOLE_0:def 3, A44;
PSI c= THETA \/ {p} by A41, XBOOLE_1:10;
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 A40, A45, XBOOLE_1:10; :: thesis: verum

end;

suppose A46: THETA \/ {('not' p)} 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 {('not' p)} by TARSKI:def 1;
then A48: ( 'not' p in THETA \/ {('not' p)} & not 'not' p in THETA ) by XBOOLE_0:def 3, A47;
PSI c= THETA \/ {('not' p)} by A41, XBOOLE_1:10;
then THETA \/ {('not' p)} 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