let CX be Consistent Subset of CQC-WFF ; :: thesis: ( CX is with_examples implies ex CY being Consistent Subset of CQC-WFF st
( CX c= CY & CY is negation_faithful & CY is with_examples ) )
assume A1: CX is with_examples ; :: thesis: ex CY being Consistent Subset of CQC-WFF st
( CX c= CY & CY is negation_faithful & CY is with_examples )
consider f being Function such that
A2: ( dom f = NAT & CQC-WFF = rng f ) by Lm1, Th19;
reconsider f = f as Function of NAT , CQC-WFF by A2, FUNCT_2:4;
defpred S1[ set , set , set ] means ex X being Subset of CQC-WFF st
( X = $2 \/ {(f . $1)} & ( X is Consistent implies $3 = X ) & ( not X is Consistent implies $3 = $2 ) );
A3: for n being Element of NAT
for C being Subset of CQC-WFF ex D being Subset of CQC-WFF st S1[n,C,D]
proof
let n be Element of NAT ; :: thesis: for C being Subset of CQC-WFF ex D being Subset of CQC-WFF st S1[n,C,D]
reconsider p = f . n as Element of CQC-WFF ;
let C be Subset of CQC-WFF ; :: thesis: ex D being Subset of CQC-WFF st S1[n,C,D]
set X = C \/ {p};
reconsider X = C \/ {p} as Subset of CQC-WFF ;
( not X is Consistent implies ex D being Subset of CQC-WFF st
( D = C & ex X being Subset of CQC-WFF 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 st S1[n,C,D] ; :: thesis: verum
end;
consider h being Function of NAT , bool CQC-WFF such that
A4: ( h . 0 = CX & ( for n being Element of NAT holds S1[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A3);
 set CY = union (rng h);
A5: now
let a be set ; :: thesis: ( a in CX implies a in union (rng h) )
assume A6: a in CX ; :: thesis: a in union (rng h)
dom h = NAT by FUNCT_2:def 1;
then ( a in h . 0 & h . 0 in rng h ) by A4, A6, FUNCT_1:12;
hence a in union (rng h) by TARSKI:def 4; :: thesis: verum
end;
then A7: CX c= union (rng h) by TARSKI:def 3;
A8: for n being Element of NAT holds h . n c= h . (n + 1)
proof
let n be Element of NAT ; :: thesis: h . n c= h . (n + 1)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in h . n or a in h . (n + 1) )
assume A9: a in h . n ; :: thesis: a in h . (n + 1)
reconsider p = f . n as Element of CQC-WFF ;
set X = (h . n) \/ {p};
reconsider X = (h . n) \/ {p} as Subset of CQC-WFF ;
A10: h . n c= X by XBOOLE_1:7;
ex Y being Subset of CQC-WFF 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 A4;
hence a in h . (n + 1) by A9, A10; :: thesis: verum
end;
A11: for n, m being Element of NAT st m in dom h & n in dom h & n < m holds
h . n c= h . m
proof
let n, m be Element of NAT ; :: thesis: ( m in dom h & n in dom h & n < m implies h . n c= h . m )
assume A12: ( m in dom h & n in dom h & n < m ) ; :: thesis: h . n c= h . m
defpred S2[ Element of NAT ] means ( n <= $1 implies h . n c= h . $1 );
A13: S2[ 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;
A14: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A15: S2[k] ; :: thesis: S2[k + 1]
assume A16: n <= k + 1 ; :: thesis: h . n c= h . (k + 1)
now
assume A17: n <= k ; :: thesis: h . n c= h . (k + 1)
h . k c= h . (k + 1) by A8;
hence h . n c= h . (k + 1) by A15, A17, XBOOLE_1:1; :: thesis: verum
end;
hence h . n c= h . (k + 1) by A16, NAT_1:8; :: thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A13, A14);
 hence h . n c= h . m by A12; :: thesis: verum
end;
defpred S2[ Element of NAT ] means h . $1 is Consistent;
A18: S2[ 0 ] by A4;
A19: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let n be Element of NAT ; :: thesis: ( S2[n] implies S2[n + 1] )
assume A20: S2[n] ; :: thesis: S2[n + 1]
ex Y being Subset of CQC-WFF 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 A4;
hence S2[n + 1] by A20; :: thesis: verum
end;
set CY = union (rng h);
for n being Element of NAT holds S2[n] from NAT_1:sch 1(A18, A19);
 then for n, m being Element of NAT st m in dom h & n in dom h & n < m holds
( h . n is Consistent & h . n c= h . m ) by A11;
then reconsider CY = union (rng h) as Consistent Subset of CQC-WFF by HENMODEL:11;
A21: CY is negation_faithful
proof
let p be Element of CQC-WFF ; :: according to GOEDELCP:def 1 :: thesis: ( CY |- p or CY |- 'not' p )
consider a being set such that
A22: ( a in dom f & f . a = p ) by A2, FUNCT_1:def 5;
reconsider n = a as Element of NAT by A22;
now
assume not CY |- 'not' p ; :: thesis: CY |- p
then A23: CY \/ {p} is Consistent by HENMODEL:10;
A24: now
assume not (h . n) \/ {p} is Consistent ; :: thesis: contradiction
then A25: (h . n) \/ {p} |- 'not' VERUM by Th24;
now
let a be set ; :: thesis: ( a in h . n implies a in CY )
assume A26: a in h . n ; :: thesis: a in CY
dom h = NAT by FUNCT_2:def 1;
then h . n in rng h by FUNCT_1:12;
hence a in CY by A26, TARSKI:def 4; :: thesis: verum
end;
then h . n c= CY by TARSKI:def 3;
then CY \/ {p} |- 'not' VERUM by A25, Th32, XBOOLE_1:9;
hence contradiction by A23, Th24; :: thesis: verum
end;
A27: ex Y being Subset of CQC-WFF 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 A4;
now
let a be set ; :: thesis: ( a in h . (n + 1) implies a in CY )
assume A28: 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:12;
hence a in CY by A28, TARSKI:def 4; :: thesis: verum
end;
then A29: h . (n + 1) c= CY by TARSKI:def 3;
{p} c= h . (n + 1) by A22, A24, A27, XBOOLE_1:7;
then {p} c= CY by A29, XBOOLE_1:1;
then p in CY by ZFMISC_1:37;
hence CY |- p by Th21; :: thesis: verum
end;
hence ( CY |- p or CY |- 'not' p ) ; :: thesis: verum
end;
A30: CY is with_examples
proof
let x be bound_QC-variable; :: according to GOEDELCP:def 2 :: thesis: for p being Element of CQC-WFF ex y being bound_QC-variable st CY |- ('not' (Ex x,p)) 'or' (p . x,y)
let p be Element of CQC-WFF ; :: thesis: ex y being bound_QC-variable st CY |- ('not' (Ex x,p)) 'or' (p . x,y)
consider y being bound_QC-variable such that
A31: CX |- ('not' (Ex x,p)) 'or' (p . x,y) by A1, Def2;
take y ; :: thesis: CY |- ('not' (Ex x,p)) 'or' (p . x,y)
thus CY |- ('not' (Ex x,p)) 'or' (p . x,y) by A7, A31, 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 A5, A21, A30, TARSKI:def 3; :: thesis: verum