let Al be QC-alphabet ; :: thesis: for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & CX is with_examples holds
ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
let CX be Consistent Subset of (CQC-WFF Al); :: thesis: ( Al is countable & CX is with_examples implies ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A1: Al is countable ; :: thesis: ( not CX is with_examples or ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A2: CX is with_examples ; :: thesis: ex CY being Consistent Subset of (CQC-WFF Al) st
( CX c= CY & CY is negation_faithful & CY is with_examples )
( not CQC-WFF Al is empty & CQC-WFF Al is countable ) by Th19, A1;
then consider f being Function such that
A3: dom f = NAT and
A4: CQC-WFF Al = rng f by Lm1;
reconsider f = f as sequence of (CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S₁[ set , set , set ] means ex X being Subset of (CQC-WFF Al) st
( X = $2 \/ {(f . $1)} & ( X is Consistent implies $3 = X ) & ( not X is Consistent implies $3 = $2 ) );
A5: for n being Nat
for C being Subset of (CQC-WFF Al) ex D being Subset of (CQC-WFF Al) st S₁[n,C,D]

proof

let n be Nat; :: thesis: for C being Subset of (CQC-WFF Al) ex D being Subset of (CQC-WFF Al) st S₁[n,C,D]
reconsider p = f . n as Element of CQC-WFF Al ;
let C be Subset of (CQC-WFF Al); :: thesis: ex D being Subset of (CQC-WFF Al) st S₁[n,C,D]
set X = C \/ {p};
reconsider X = C \/ {p} as Subset of (CQC-WFF Al) ;
( not X is Consistent implies ex D being Subset of (CQC-WFF Al) st
( D = C & ex X being Subset of (CQC-WFF Al) st
( X = C \/ {p} & ( X is Consistent implies D = X ) & ( not X is Consistent implies D = C ) ) ) ) ;
hence ex D being Subset of (CQC-WFF Al) st S₁[n,C,D] ; :: thesis: verum

end;

consider h being sequence of (bool (CQC-WFF Al)) such that
A6: ( h . 0 = CX & ( for n being Nat holds S₁[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A5);
set CY = union (rng h);

A7: now :: thesis: for a being object st a in CX holds
a in union (rng h)

let a be object ; :: thesis: ( a in CX implies a in union (rng h) )
assume A8: a in CX ; :: thesis: a in union (rng h)
dom h = NAT by FUNCT_2:def 1;
then h . 0 in rng h by FUNCT_1:3;
hence a in union (rng h) by A6, A8, TARSKI:def 4; :: thesis: verum

end;

then A9: CX c= union (rng h) ;
A10: for n being Nat holds h . n c= h . (n + 1)

proof

let n be Nat; :: thesis: h . n c= h . (n + 1)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in h . n or a in h . (n + 1) )
assume A11: a in h . n ; :: thesis: a in h . (n + 1)
reconsider p = f . n as Element of CQC-WFF Al ;
set X = (h . n) \/ {p};
reconsider X = (h . n) \/ {p} as Subset of (CQC-WFF Al) ;
A12: h . n c= X by XBOOLE_1:7;
ex Y being Subset of (CQC-WFF Al) st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A6;
hence a in h . (n + 1) by A11, A12; :: thesis: verum

end;

A13: for n, m being Nat st m in dom h & n in dom h & n < m holds
h . n c= h . m

proof

let n, m be Nat; :: thesis: ( m in dom h & n in dom h & n < m implies h . n c= h . m )
assume that
m in dom h and
n in dom h and
A14: n < m ; :: thesis: h . n c= h . m
defpred S₂[ Nat] means ( n <= $1 implies h . n c= h . $1 );
A15: S₂[ 0 ]

proof

assume n <= 0 ; :: thesis: h . n c= h . 0
then n = 0 by NAT_1:2;
hence h . n c= h . 0 ; :: thesis: verum

end;

A16: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A17: S₂[k] ; :: thesis: S₂[k + 1]
assume A18: n <= k + 1 ; :: thesis: h . n c= h . (k + 1)

now :: thesis: ( n <= k implies h . n c= h . (k + 1) )

assume A19: n <= k ; :: thesis: h . n c= h . (k + 1)
h . k c= h . (k + 1) by A10;
hence h . n c= h . (k + 1) by A17, A19; :: thesis: verum

end;

hence h . n c= h . (k + 1) by A18, NAT_1:8; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A15, A16);
hence h . n c= h . m by A14; :: thesis: verum

end;

defpred S₂[ Nat] means h . $1 is Consistent ;
A20: S₂[ 0 ] by A6;
A21: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A22: S₂[n] ; :: thesis: S₂[n + 1]
ex Y being Subset of (CQC-WFF Al) st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A6;
hence S₂[n + 1] by A22; :: thesis: verum

end;

set CY = union (rng h);
for n being Nat holds S₂[n] from NAT_1:sch 2(A20, A21);
then for n, m being Nat st m in dom h & n in dom h & n < m holds
( h . n is Consistent & h . n c= h . m ) by A13;
then reconsider CY = union (rng h) as Consistent Subset of (CQC-WFF Al) by HENMODEL:11;
A23: CY is negation_faithful

proof

let p be Element of CQC-WFF Al; :: according to GOEDELCP:def 1 :: thesis: ( CY |- p or CY |- 'not' p )
consider a being object such that
A24: a in dom f and
A25: f . a = p by A4, FUNCT_1:def 3;
reconsider n = a as Nat by A24;

now :: thesis: ( not CY |- 'not' p implies CY |- p )

assume not CY |- 'not' p ; :: thesis: CY |- p
then A26: not CY \/ {p} is Inconsistent by HENMODEL:10;

A27: now :: thesis: not (h . n) \/ {p} is Inconsistent

assume (h . n) \/ {p} is Inconsistent ; :: thesis: contradiction
then A28: (h . n) \/ {p} |- 'not' (VERUM Al) by Th24;

now :: thesis: for a being object st a in h . n holds
a in CY

let a be object ; :: thesis: ( a in h . n implies a in CY )
assume A29: a in h . n ; :: thesis: a in CY
A30: n in NAT by ORDINAL1:def 12;
dom h = NAT by FUNCT_2:def 1;
then h . n in rng h by FUNCT_1:3, A30;
hence a in CY by A29, TARSKI:def 4; :: thesis: verum

end;

then h . n c= CY ;
then CY \/ {p} |- 'not' (VERUM Al) by A28, Th32, XBOOLE_1:9;
hence contradiction by A26, Th24; :: thesis: verum

end;

A31: ex Y being Subset of (CQC-WFF Al) st
( Y = (h . n) \/ {(f . n)} & ( Y is Consistent implies h . (n + 1) = Y ) & ( not Y is Consistent implies h . (n + 1) = h . n ) ) by A6;

now :: thesis: for a being object st a in h . (n + 1) holds
a in CY

let a be object ; :: thesis: ( a in h . (n + 1) implies a in CY )
assume A32: a in h . (n + 1) ; :: thesis: a in CY
dom h = NAT by FUNCT_2:def 1;
then h . (n + 1) in rng h by FUNCT_1:3;
hence a in CY by A32, TARSKI:def 4; :: thesis: verum

end;

then A33: h . (n + 1) c= CY ;
{p} c= h . (n + 1) by A25, A27, A31, XBOOLE_1:7;
then {p} c= CY by A33;
then p in CY by ZFMISC_1:31;
hence CY |- p by Th21; :: thesis: verum

end;

hence ( CY |- p or CY |- 'not' p ) ; :: thesis: verum

end;

A34: CY is with_examples

proof

let x be bound_QC-variable of Al; :: according to GOEDELCP:def 2 :: thesis: for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF Al; :: thesis: ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
consider y being bound_QC-variable of Al such that
A35: CX |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A2;
take y ; :: thesis: CY |- ('not' (Ex (x,p))) 'or' (p . (x,y))
thus CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A9, A35, Th32; :: thesis: verum

end;

take CY ; :: thesis: ( CX c= CY & CY is negation_faithful & CY is with_examples )
thus ( CX c= CY & CY is negation_faithful & CY is with_examples ) by A7, A23, A34; :: thesis: verum