let CX be Consistent Subset of CQC-WFF; :: thesis:
assume A1: still_not-bound_in CX is finite ; :: thesis:
consider f being Function such that
A2: dom f = NAT and
A3: ExCl = rng f by Lm1, Th20;
reconsider f = f as Function of NAT,CQC-WFF by A2, A3, FUNCT_2:2;
defpred S₁[ Element of NAT , set , set ] means ex K, L being Subset of bound_QC-variables st
( K = $2 `2 & L = K \/ (still_not-bound_in {(f . ($1 + 1))}) & $3 = [(('not' (f . ($1 + 1))) 'or' ((the_scope_of (f,($1 + 1))) . ((bound_in (f,($1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in L } ))))),(K \/ (still_not-bound_in (('not' (f . ($1 + 1))) 'or' ((the_scope_of (f,($1 + 1))) . ((bound_in (f,($1 + 1))),(x. (min* { j where j is Element of NAT : not x. j in L } )))))))] );
A4: for n being Element of NAT
for C being Element of [:CQC-WFF,(bool bound_QC-variables):] ex D being Element of [:CQC-WFF,(bool bound_QC-variables):] st S₁[n,C,D]

let n be Element of NAT ; :: thesis:
let C be Element of [:CQC-WFF,(bool bound_QC-variables):]; :: thesis:
set K = C `2 ;
ex a, b being set st
( a in CQC-WFF & b in bool bound_QC-variables & C = [a,b] ) by ZFMISC_1:def 2;
then reconsider K = C `2 as Subset of bound_QC-variables by MCART_1:7;
set L = K \/ (still_not-bound_in {(f . (n + 1))});
set D = [(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))];
take [(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))] ; :: thesis:
thus S₁[n,C,[(('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (n + 1))}) } ))))),(K \/ (still_not-bound_in (('not' (f . (n + 1))) 'or' ((the_scope_of (f,(n + 1))) . ((bound_in (f,(n + 1))),(x. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (n + 1))}) } )))))))]] ; :: thesis:

end;

reconsider A = [(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {(f . 0)}) } ))))),(still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0)}) } )))))}))] as Element of [:CQC-WFF,(bool bound_QC-variables):] ;
consider h being Function of NAT,[:CQC-WFF,(bool bound_QC-variables):] such that
A5: ( h . 0 = A & ( for n being Element of NAT holds S₁[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A4);
set CY = CX \/ { ((h . n) `1) where n is Element of NAT : verum } ;

now

let a be set ; :: thesis:
assume A6: a in CX \/ { ((h . n) `1) where n is Element of NAT : verum } ; :: thesis:

now

assume not a in CX ; :: thesis:
then a in { ((h . n) `1) where n is Element of NAT : verum } by A6, XBOOLE_0:def 3;
then consider n being Element of NAT such that
A7: a = (h . n) `1 ;
ex c, d being set st
( c in CQC-WFF & d in bool bound_QC-variables & h . n = [c,d] ) by ZFMISC_1:def 2;
hence a in CQC-WFF by A7, MCART_1:7; :: thesis:

end;

hence a in CQC-WFF ; :: thesis:

end;

then reconsider CY = CX \/ { ((h . n) `1) where n is Element of NAT : verum } as Subset of CQC-WFF by TARSKI:def 3;

A8: now

let x be bound_QC-variable; :: thesis:
let p be Element of CQC-WFF ; :: thesis:
Ex (x,p) in ExCl by Def3;
then consider a being set such that
A9: a in dom f and
A10: f . a = Ex (x,p) by A3, FUNCT_1:def 3;
reconsider a = a as Element of NAT by A9;
reconsider r9 = f . a as Element of CQC-WFF ;
A11: Ex-bound_in r9 = x by A10, Th22;
A12: Ex-the_scope_of r9 = p by A10, Th22;
A13: bound_in (f,a) = x by A11, Def6;
A14: the_scope_of (f,a) = p by A12, Def7;
A15: (h . a) `1 in { ((h . n) `1) where n is Element of NAT : verum } ;
A16: { ((h . n) `1) where n is Element of NAT : verum } c= CY by XBOOLE_1:7;

A17: now

assume A18: a = 0 ; :: thesis:
take y = x. (min* { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r9}) } ); :: thesis:
(h . a) `1 = ('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),y)) by A5, A18, MCART_1:7;
hence CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A10, A13, A14, A15, A16, Th21; :: thesis:

end;

now

assume a <> 0 ; :: thesis:
then consider m being Nat such that
A19: a = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A20: ex K, L being Subset of bound_QC-variables st
( K = (h . m) `2 & L = K \/ (still_not-bound_in {r9}) & h . a = [(('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),(x. (min* { i where i is Element of NAT : not x. i in L } ))))),(K \/ (still_not-bound_in (('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),(x. (min* { j where j is Element of NAT : not x. j in L } )))))))] ) by A5, A19;
set K = (h . m) `2 ;
set L = (still_not-bound_in {r9}) \/ ((h . m) `2);
take y = x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {r9}) \/ ((h . m) `2) } ); :: thesis:
(h . a) `1 = ('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),y)) by A20, MCART_1:7;
hence CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A10, A13, A14, A15, A16, Th21; :: thesis:

end;

hence ex y being bound_QC-variable st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A17; :: thesis:

end;

deffunc H₁( set ) -> set = CX \/ { ((h . n) `1) where n is Element of NAT : n in $1 } ;
consider F being Function such that
A21: ( dom F = NAT & ( for a being set st a in NAT holds
F . a = H₁(a) ) ) from FUNCT_1:sch 3();
A22: CY c= union (rng F)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: a in CY ; :: thesis:

A24: now

assume A25: a in CX ; :: thesis:
A26: F . 0 = CX \/ { ((h . n) `1) where n is Element of NAT : n in 0 } by A21;

now

let b be set ; :: thesis:
assume b in { ((h . n) `1) where n is Element of NAT : n in 0 } ; :: thesis:
then ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence contradiction ; :: thesis:

end;

then A27: { ((h . n) `1) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
F . 0 in rng F by A21, FUNCT_1:3;
hence a in union (rng F) by A25, A26, A27, TARSKI:def 4; :: thesis:

end;

now

assume a in { ((h . n) `1) where n is Element of NAT : verum } ; :: thesis:
then consider n being Element of NAT such that
A28: a = (h . n) `1 ;
n < n + 1 by NAT_1:13;
then n in n + 1 by NAT_1:44;
then A29: a in { ((h . m) `1) where m is Element of NAT : m in n + 1 } by A28;
F . (n + 1) = CX \/ { ((h . m) `1) where m is Element of NAT : m in n + 1 } by A21;
then A30: { ((h . m) `1) where m is Element of NAT : m in n + 1 } c= F . (n + 1) by XBOOLE_1:7;
F . (n + 1) in rng F by A21, FUNCT_1:3;
hence a in union (rng F) by A29, A30, TARSKI:def 4; :: thesis:

end;

hence a in union (rng F) by A23, A24, XBOOLE_0:def 3; :: thesis:

end;

union (rng F) c= CY

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in union (rng F) ; :: thesis:
then consider b being set such that
A31: a in b and
A32: b in rng F by TARSKI:def 4;
consider c being set such that
A33: c in dom F and
A34: F . c = b by A32, FUNCT_1:def 3;
reconsider n = c as Element of NAT by A21, A33;
A35: a in CX \/ { ((h . m) `1) where m is Element of NAT : m in n } by A21, A31, A34;

A36: now

assume A37: a in CX ; :: thesis:
CX c= CY by XBOOLE_1:7;
hence a in CY by A37; :: thesis:

end;

now

assume a in { ((h . m) `1) where m is Element of NAT : m in n } ; :: thesis:
then ex m being Element of NAT st
( a = (h . m) `1 & m in n ) ;
then A38: a in { ((h . i) `1) where i is Element of NAT : verum } ;
{ ((h . i) `1) where i is Element of NAT : verum } c= CY by XBOOLE_1:7;
hence a in CY by A38; :: thesis:

end;

hence a in CY by A35, A36, XBOOLE_0:def 3; :: thesis:

end;

then A39: CY = union (rng F) by A22, XBOOLE_0:def 10;
A40: for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
F . n c= F . m

proof

let n, m be Element of NAT ; :: thesis:
assume that
m in dom F and
n in dom F and
A41: n < m ; :: thesis:
A42: F . n = CX \/ { ((h . i) `1) where i is Element of NAT : i in n } by A21;
A43: F . m = CX \/ { ((h . i) `1) where i is Element of NAT : i in m } by A21;

now

let a be set ; :: thesis:
assume A44: a in F . n ; :: thesis:

A45: now

assume A46: a in CX ; :: thesis:
CX c= F . m by A43, XBOOLE_1:7;
hence a in F . m by A46; :: thesis:

end;

now

assume a in { ((h . i) `1) where i is Element of NAT : i in n } ; :: thesis:
then consider i being Element of NAT such that
A47: (h . i) `1 = a and
A48: i in n ;
i < n by A48, NAT_1:44;
then i < m by A41, XXREAL_0:2;
then i in m by NAT_1:44;
then A49: a in { ((h . j) `1) where j is Element of NAT : j in m } by A47;
{ ((h . j) `1) where j is Element of NAT : j in m } c= F . m by A43, XBOOLE_1:7;
hence a in F . m by A49; :: thesis:

end;

hence a in F . m by A42, A44, A45, XBOOLE_0:def 3; :: thesis:

end;

hence F . n c= F . m by TARSKI:def 3; :: thesis:

end;

rng F c= bool CQC-WFF

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then consider b being set such that
A50: b in dom F and
A51: F . b = a by FUNCT_1:def 3;
reconsider b = b as Element of NAT by A21, A50;
A52: F . b = CX \/ { ((h . i) `1) where i is Element of NAT : i in b } by A21;

now

let c be set ; :: thesis:
assume c in { ((h . i) `1) where i is Element of NAT : i in b } ; :: thesis:
then ex i being Element of NAT st
( (h . i) `1 = c & i in b ) ;
hence c in CQC-WFF by MCART_1:10; :: thesis:

end;

then { ((h . i) `1) where i is Element of NAT : i in b } c= CQC-WFF by TARSKI:def 3;
then F . b c= CQC-WFF by A52, XBOOLE_1:8;
hence a in bool CQC-WFF by A51; :: thesis:

end;

then reconsider F = F as Function of NAT,(bool CQC-WFF) by A21, FUNCT_2:2;
A53: for n being Element of NAT holds F . (n + 1) = (F . n) \/ {((h . n) `1)}

proof

let n be Element of NAT ; :: thesis:

now

let a be set ; :: thesis:
assume a in { ((h . i) `1) where i is Element of NAT : i in n + 1 } ; :: thesis:
then consider j being Element of NAT such that
A54: a = (h . j) `1 and
A55: j in n + 1 ;
j < n + 1 by A55, NAT_1:44;
then A56: j + 1 <= n + 1 by NAT_1:13;

A57: now

assume j + 1 = n + 1 ; :: thesis:
then A58: a in {((h . n) `1)} by A54, TARSKI:def 1;
{((h . n) `1)} c= { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by XBOOLE_1:7;
hence a in { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by A58; :: thesis:

end;

now

assume j + 1 <= n ; :: thesis:
then j < n by NAT_1:13;
then j in n by NAT_1:44;
then A59: a in { ((h . k) `1) where k is Element of NAT : k in n } by A54;
{ ((h . k) `1) where k is Element of NAT : k in n } c= { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by XBOOLE_1:7;
hence a in { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by A59; :: thesis:

end;

hence a in { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by A56, A57, NAT_1:8; :: thesis:

end;

then A60: { ((h . k) `1) where k is Element of NAT : k in n + 1 } c= { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} by TARSKI:def 3;

now

let a be set ; :: thesis:
assume A61: a in { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} ; :: thesis:

A62: now

assume a in { ((h . i) `1) where i is Element of NAT : i in n } ; :: thesis:
then consider j being Element of NAT such that
A63: (h . j) `1 = a and
A64: j in n ;
A65: n <= n + 1 by NAT_1:11;
j < n by A64, NAT_1:44;
then j < n + 1 by A65, XXREAL_0:2;
then j in n + 1 by NAT_1:44;
hence a in { ((h . i) `1) where i is Element of NAT : i in n + 1 } by A63; :: thesis:

end;

now

assume a in {((h . n) `1)} ; :: thesis:
then A66: a = (h . n) `1 by TARSKI:def 1;
n < n + 1 by NAT_1:13;
then n in n + 1 by NAT_1:44;
hence a in { ((h . i) `1) where i is Element of NAT : i in n + 1 } by A66; :: thesis:

end;

hence a in { ((h . i) `1) where i is Element of NAT : i in n + 1 } by A61, A62, XBOOLE_0:def 3; :: thesis:

end;

then { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} c= { ((h . k) `1) where k is Element of NAT : k in n + 1 } by TARSKI:def 3;
then { ((h . i) `1) where i is Element of NAT : i in n } \/ {((h . n) `1)} = { ((h . k) `1) where k is Element of NAT : k in n + 1 } by A60, XBOOLE_0:def 10;
then F . (n + 1) = CX \/ ( { ((h . k) `1) where k is Element of NAT : k in n } \/ {((h . n) `1)}) by A21;
then F . (n + 1) = (CX \/ { ((h . k) `1) where k is Element of NAT : k in n } ) \/ {((h . n) `1)} by XBOOLE_1:4;
hence F . (n + 1) = (F . n) \/ {((h . n) `1)} by A21; :: thesis:

end;

defpred S₂[ Element of NAT ] means ( (h . $1) `2 is finite & (h . $1) `2 is Subset of bound_QC-variables );
A67: S₂[ 0 ]

proof

A68: (h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0)}) } )))))}) by A5, MCART_1:7;
reconsider s = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { j where j is Element of NAT : not x. j in still_not-bound_in (CX \/ {(f . 0)}) } )))) as Element of CQC-WFF ;
still_not-bound_in s is finite by CQC_SIM1:19;
then still_not-bound_in {s} is finite by Th26;
then (still_not-bound_in {s}) \/ (still_not-bound_in CX) is finite by A1;
hence S₂[ 0 ] by A68, Th27; :: thesis:

end;

A69: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A70: S₂[k] ; :: thesis:
A71: ex K, L being Subset of bound_QC-variables st
( K = (h . k) `2 & L = K \/ (still_not-bound_in {(f . (k + 1))}) & h . (k + 1) = [(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { i where i is Element of NAT : not x. i in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { j where j is Element of NAT : not x. j in L } )))))))] ) by A5;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of bound_QC-variables by A70;
set L = K \/ (still_not-bound_in {(f . (k + 1))});
set s = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (k + 1))}) } ))));
still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { j where j is Element of NAT : not x. j in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) is finite by CQC_SIM1:19;
hence S₂[k + 1] by A70, A71, MCART_1:7; :: thesis:

end;

A72: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A67, A69);
defpred S₃[ Element of NAT ] means ( still_not-bound_in (F . ($1 + 1)) c= (h . $1) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2) } ) in still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}) );
A73: for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )

proof

A74: S₃[ 0 ]

proof

set r = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0)}) } ))));
set A1 = {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0)}) } )))))};
reconsider s = f . 1 as Element of CQC-WFF ;
A75: (h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0)}) } )))))}) by A5, MCART_1:7;
reconsider B = (h . 0) `2 as Subset of bound_QC-variables by A5, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool bound_QC-variables ;
still_not-bound_in s is finite by CQC_SIM1:19;
then still_not-bound_in {s} is finite by Th26;
then consider x being bound_QC-variable such that
A76: not x in C by A67, Th28;
consider l being Element of NAT such that
A77: x. l = x by QC_LANG3:30;
l in { i where i is Element of NAT : not x. i in C } by A76, A77;
then reconsider A = { i where i is Element of NAT : not x. i in C } as non empty set ;

now

let a be set ; :: thesis:
assume a in A ; :: thesis:
then ex i being Element of NAT st
( a = i & not x. i in C ) ;
hence a in NAT ; :: thesis:

end;

then reconsider A = { i where i is Element of NAT : not x. i in C } as non empty Subset of NAT by TARSKI:def 3;
set j = min* A;
min* A in A by NAT_1:def 1;
then A78: ex i being Element of NAT st
( i = min* A & not x. i in C ) ;
A79: F . 0 = CX \/ { ((h . n) `1) where n is Element of NAT : n in 0 } by A21;

now

let b be set ; :: thesis:
assume b in { ((h . n) `1) where n is Element of NAT : n in 0 } ; :: thesis:
then ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence contradiction ; :: thesis:

end;

then A80: { ((h . n) `1) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
(h . 0) `1 = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0)}) } )))) by A5, MCART_1:7;
then F . (0 + 1) = CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (min* { k where k is Element of NAT : not x. k in still_not-bound_in (CX \/ {(f . 0)}) } )))))} by A53, A79, A80;
hence S₃[ 0 ] by A75, A78, Th27; :: thesis:

end;

A81: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A82: S₃[k] ; :: thesis:
reconsider s = f . (k + 2) as Element of CQC-WFF ;
A83: ex K, L being Subset of bound_QC-variables st
( K = (h . k) `2 & L = K \/ (still_not-bound_in {(f . (k + 1))}) & h . (k + 1) = [(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { i where i is Element of NAT : not x. i in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { j where j is Element of NAT : not x. j in L } )))))))] ) by A5;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of bound_QC-variables by A72;
set L = K \/ (still_not-bound_in {(f . (k + 1))});
set r = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } ))));
A84: (h . (k + 1)) `1 = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } )))) by A83, MCART_1:7;
A85: (h . (k + 1)) `2 = K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (min* { i where i is Element of NAT : not x. i in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))) by A83, MCART_1:7;
reconsider B = (h . (k + 1)) `2 as Subset of bound_QC-variables by A83, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool bound_QC-variables ;
still_not-bound_in s is finite by CQC_SIM1:19;
then A86: still_not-bound_in {s} is finite by Th26;
(h . (k + 1)) `2 is finite by A72;
then consider x being bound_QC-variable such that
A87: not x in C by A86, Th28;
consider l being Element of NAT such that
A88: x. l = x by QC_LANG3:30;
l in { i where i is Element of NAT : not x. i in (still_not-bound_in {s}) \/ B } by A87, A88;
then reconsider A = { i where i is Element of NAT : not x. i in (still_not-bound_in {s}) \/ B } as non empty set ;

now

let a be set ; :: thesis:
assume a in A ; :: thesis:
then ex i being Element of NAT st
( a = i & not x. i in C ) ;
hence a in NAT ; :: thesis:

end;

end;

for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A74, A81);
hence for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (min* { i where i is Element of NAT : not x. i in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) ) ; :: thesis:

end;

defpred S₄[ Element of NAT ] means F . $1 is Consistent ;

now

let a be set ; :: thesis:
assume a in { ((h . i) `1) where i is Element of NAT : i in 0 } ; :: thesis:
then ex j being Element of NAT st
( a = (h . j) `1 & j in 0 ) ;
hence contradiction ; :: thesis:

end;

then { ((h . i) `1) where i is Element of NAT : i in 0 } = {} by XBOOLE_0:def 1;
then A92: F . 0 = CX \/ {} by A21;
then A93: S₄[ 0 ] ;
A94: for k being Element of NAT st S₄[k] holds
S₄[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A95: S₄[k] ; :: thesis:
ex c, d being set st
( c in CQC-WFF & d in bool bound_QC-variables & h . k = [c,d] ) by ZFMISC_1:def 2;
then reconsider r = (h . k) `1 as Element of CQC-WFF by MCART_1:7;

now

assume not F . (k + 1) is Consistent ; :: thesis:
then F . (k + 1) |- 'not' VERUM by HENMODEL:6;
then (F . k) \/ {r} |- 'not' VERUM by A53;
then consider f1 being FinSequence of CQC-WFF such that
A96: rng f1 c= F . k and
A97: |- (f1 ^ <*r*>) ^ <*('not' VERUM)*> by HENMODEL:8;
A98: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (f . k))*> by CALCUL_2:21;

A99: now

now

let a be set ; :: thesis:
assume a in A ; :: thesis:
then ex i being Element of NAT st
( a = i & not x. i in still_not-bound_in (CX \/ {r1}) ) ;
hence a in NAT ; :: thesis:

end;

then reconsider A = { i where i is Element of NAT : not x. i in still_not-bound_in (CX \/ {r1}) } as non empty Subset of NAT by TARSKI:def 3;
set j = min* A;
min* A in A by NAT_1:def 1;
then consider i being Element of NAT such that
A108: i = min* A and
A109: not x. i in still_not-bound_in (CX \/ {r1}) ;
A110: not x. i in (still_not-bound_in CX) \/ (still_not-bound_in {r1}) by A109, Th27;
then A111: not x. i in still_not-bound_in {r1} by XBOOLE_0:def 3;
A112: F . 0 = CX \/ { ((h . n) `1) where n is Element of NAT : n in 0 } by A21;

now

let b be set ; :: thesis:
assume b in { ((h . n) `1) where n is Element of NAT : n in 0 } ; :: thesis:
then ex n being Element of NAT st
( b = (h . n) `1 & n in 0 ) ;
hence contradiction ; :: thesis:

end;

then { ((h . n) `1) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
then still_not-bound_in (rng f1) c= still_not-bound_in CX by A96, A100, A112, Th29;
then not x. i in still_not-bound_in (rng f1) by A110, XBOOLE_0:def 3;
then A113: not x. (min* A) in still_not-bound_in f1 by A108, Th30;
reconsider r2 = the_scope_of (f,0) as Element of CQC-WFF ;
reconsider y2 = bound_in (f,0) as bound_QC-variable ;
r1 in ExCl by A2, A3, FUNCT_1:3;
then consider y1 being bound_QC-variable, s1 being Element of CQC-WFF such that
A114: r1 = Ex (y1,s1) by Def3;
A115: s1 = Ex-the_scope_of r1 by A114, Th22;
A116: r2 = Ex-the_scope_of r1 by Def7;
A117: y1 = Ex-bound_in r1 by A114, Th22;
A118: y2 = Ex-bound_in r1 by Def6;
not x. (min* A) in still_not-bound_in r1 by A108, A111, Th26;
then not x. (min* A) in still_not-bound_in <*r1*> by CALCUL_1:60;
then not x. (min* A) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A113, XBOOLE_0:def 3;
then A119: not x. (min* A) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
not x. (min* A) in still_not-bound_in ('not' VERUM) by QC_LANG3:3, QC_LANG3:7;
then not x. (min* A) in still_not-bound_in <*('not' VERUM)*> by CALCUL_1:60;
then not x. (min* A) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' VERUM)*>) by A119, XBOOLE_0:def 3;
then not x. (min* A) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' VERUM)*>) by CALCUL_1:59;
then |- (f1 ^ <*r1*>) ^ <*('not' VERUM)*> by A105, A114, A115, A116, A117, A118, CALCUL_1:61;
then |- f1 ^ <*('not' VERUM)*> by A100, A103, CALCUL_2:26;
then F . k |- 'not' VERUM by A96, HENMODEL:def 1;
hence contradiction by A92, A100, Th24; :: thesis:

end;

now

assume k <> 0 ; :: thesis:
then consider k1 being Nat such that
A120: k = k1 + 1 by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
A121: ex K, L being Subset of bound_QC-variables st
( K = (h . k1) `2 & L = K \/ (still_not-bound_in {(f . (k1 + 1))}) & h . (k1 + 1) = [(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { j where j is Element of NAT : not x. j in L } )))))))] ) by A5;
set K = (h . k1) `2 ;
set r1 = f . (k1 + 1);
set L = ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))});
set p1 = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))));
A122: r = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))) by A120, A121, MCART_1:7;
reconsider s = (the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))) as Element of CQC-WFF ;
A123: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*> by A98, A120, CALCUL_1:51;
0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then |- (((Ant (f1 ^ <*r*>)) ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM)*> by A97, Th25;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM)*> by CALCUL_1:5;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*r*>) ^ <*('not' VERUM)*> by CALCUL_1:5;
then A124: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' VERUM)*> by A122, A123, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A125: |- (f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*> by CALCUL_1:52;
0 + 1 <= len (f1 ^ <*r*>) by CALCUL_1:10;
then |- (((Ant (f1 ^ <*r*>)) ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM)*> by A97, Th25;
then |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' VERUM)*> by CALCUL_1:5;
then |- ((f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*>) ^ <*('not' VERUM)*> by A122, CALCUL_1:5;
then A126: |- (f1 ^ <*s*>) ^ <*('not' VERUM)*> by A125, CALCUL_2:24;
set y = x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } );
set j = min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ;
reconsider r2 = the_scope_of (f,(k1 + 1)) as Element of CQC-WFF ;
reconsider y2 = bound_in (f,(k1 + 1)) as bound_QC-variable ;
reconsider r1 = f . (k1 + 1) as Element of CQC-WFF ;
r1 in ExCl by A2, A3, FUNCT_1:3;
then consider y1 being bound_QC-variable, s1 being Element of CQC-WFF such that
A127: r1 = Ex (y1,s1) by Def3;
A128: s1 = Ex-the_scope_of r1 by A127, Th22;
A129: r2 = Ex-the_scope_of r1 by Def7;
A130: y1 = Ex-bound_in r1 by A127, Th22;
A131: y2 = Ex-bound_in r1 by Def6;
reconsider Z = F . k as Subset of CQC-WFF ;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (Z \/ {r1}) by A73, A120;
then A132: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in Z) \/ (still_not-bound_in {r1}) by Th27;
then A133: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in {r1} by XBOOLE_0:def 3;
still_not-bound_in (rng f1) c= still_not-bound_in Z by A96, Th29;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (rng f1) by A132, XBOOLE_0:def 3;
then A134: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in f1 by Th30;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in r1 by A133, Th26;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*r1*> by CALCUL_1:60;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A134, XBOOLE_0:def 3;
then A135: not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ('not' VERUM) by QC_LANG3:3, QC_LANG3:7;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*('not' VERUM)*> by CALCUL_1:60;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' VERUM)*>) by A135, XBOOLE_0:def 3;
then not x. (min* { i where i is Element of NAT : not x. i in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' VERUM)*>) by CALCUL_1:59;
then |- (f1 ^ <*r1*>) ^ <*('not' VERUM)*> by A126, A127, A128, A129, A130, A131, CALCUL_1:61;
then |- f1 ^ <*('not' VERUM)*> by A124, CALCUL_2:26;
then F . k |- 'not' VERUM by A96, HENMODEL:def 1;
hence contradiction by A95, Th24; :: thesis:

end;

hence contradiction by A99; :: thesis:

end;

hence S₄[k + 1] ; :: thesis:

end;

for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A93, A94);
then for n, m being Element of NAT st m in dom F & n in dom F & n < m holds
( F . n is Consistent & F . n c= F . m ) by A40;
then reconsider CY = CY as Consistent Subset of CQC-WFF by A39, HENMODEL:11;
take CY ; :: thesis:
thus ( CX c= CY & CY is with_examples ) by A8, Def2, XBOOLE_1:7; :: thesis: