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 ) )

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 )

( THETA |- p or THETA |- 'not' p )

hence ex THETA being Consistent Subset of (CQC-WFF Al) st

( THETA is negation_faithful & PSI c= THETA ) by A41; :: thesis: verum

( 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

then consider THETA being set such that
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 ) )

end;( 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 )
;

end;

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 ) )

( 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;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

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 ) )

( 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

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;A5: PSI c= union Z

proof

A8:
union Z is Consistent Subset of (CQC-WFF Al)
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;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

proof

( 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
for X being set st X in Z holds

X c= CQC-WFF Al

Y is Consistent

end;X c= CQC-WFF Al

proof

then reconsider Y = union Z as Subset of (CQC-WFF Al) by ZFMISC_1:76;
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;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

Y is Consistent

proof

hence
union Z is Consistent Subset of (CQC-WFF Al)
; :: thesis: verum
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 )

A22: for x being set st x in X holds

ex R being set st

( R in Rs & x in R ) ;

defpred S_{1}[ set ] means ( not $1 is empty implies union $1 in $1 );

A23: Rs is finite ;

A24: S_{1}[ {} ]
;

A25: for x, B being set st x in Rs & B c= Rs & S_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[Rs]
from FINSET_1:sch 2(A23, A24, A25);

not X is empty

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

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;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

then consider Rs being finite Subset of Z such that
defpred S_{1}[ 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_{1}[ {} ]
_{1}[B] holds

S_{1}[B \/ {x}]

S_{1}[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;for x being set st x in $1 holds

ex R being set st

( R in Rs & x in R );

A11: S

proof

A13:
for x, B being set st x in X & B c= X & S
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_{1}[ {} ]
; :: thesis: verum

end;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

S

proof

A21:
X is finite
by A10;
let x, B be set ; :: thesis: ( x in X & B c= X & S_{1}[B] implies S_{1}[B \/ {x}] )

assume A14: ( x in X & B c= X & S_{1}[B] )
; :: thesis: S_{1}[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 )_{1}[B \/ {x}]
by A17; :: thesis: verum

end;assume A14: ( x in X & B c= X & S

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

hence
S
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 )

end;( 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;

end;

S

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

A22: for x being set st x in X holds

ex R being set st

( R in Rs & x in R ) ;

defpred S

A23: Rs is finite ;

A24: S

A25: for x, B being set st x in Rs & B c= Rs & S

S

proof

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

assume A26: ( x in Rs & B c= Rs & S_{1}[B] )
; :: thesis: S_{1}[B \/ {x}]

end;assume A26: ( x in Rs & B c= Rs & S

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

end;

suppose A27:
B is empty
; :: thesis: S_{1}[B \/ {x}]

A28:
union (B \/ {x}) = x
by A27, ZFMISC_1:25;

thus S_{1}[B \/ {x}]
by A27, A28, TARSKI:def 1; :: thesis: verum

end;thus S

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

end;

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

end;

suppose A30:
x c= union B
; :: thesis: S_{1}[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_{1}[B \/ {x}]
by A26, A29, XBOOLE_0:def 3; :: thesis: verum

end;.= (union B) \/ x by ZFMISC_1:25

.= union B by A30, XBOOLE_1:12 ;

hence S

suppose A31:
union B c= x
; :: thesis: S_{1}[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_{1}[B \/ {x}]
by A32, XBOOLE_0:def 3; :: thesis: verum

end;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

not X is empty

proof

then consider x being object such that
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;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

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

then A38:
X c= uRs
;
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;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

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

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

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

for p being Element of CQC-WFF Al holds
let p be Element of CQC-WFF Al; :: thesis: ( p in THETA or 'not' p in THETA )

end;per cases
( THETA \/ {p} is Consistent or THETA \/ {('not' p)} is Consistent )
by Th11;

end;

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;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

suppose A46:
THETA \/ {('not' p)} is Consistent
; :: thesis: ( p in THETA or 'not' p in THETA )

'not' p in THETA

end;proof

hence
( p in THETA or 'not' p in THETA )
; :: thesis: verum
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;'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

( THETA |- p or THETA |- 'not' p )

proof

then
THETA is negation_faithful
by GOEDELCP:def 1;
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;( p in THETA or 'not' p in THETA ) by A42;

hence ( THETA |- p or THETA |- 'not' p ) by GOEDELCP:21; :: thesis: verum

hence ex THETA being Consistent Subset of (CQC-WFF Al) st

( THETA is negation_faithful & PSI c= THETA ) by A41; :: thesis: verum