let Al be QC-alphabet ; :: thesis:
let CX be Consistent Subset of (CQC-WFF Al); :: thesis:
assume A1: Al is countable ; :: thesis:
assume A2: still_not-bound_in CX is finite ; :: thesis:
( not ExCl Al is empty & ExCl Al is countable ) by A1, Th20;
then consider f being Function such that
A3: dom f = NAT and
A4: ExCl Al = rng f by Lm1;
reconsider f = f as Function of NAT,(CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S₁[ Element of NAT , set , set ] means ex K, L being Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . ($1 + 1))) 'or' ((the_scope_of (f,($1 + 1))) . ((bound_in (f,($1 + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] );
A5: for n being Element of NAT
for C being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ex D being Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] st S₁[n,C,D]

let n be Element of NAT ; :: thesis:
let C be Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]; :: thesis:
set K = C `2 ;
ex a, b being set st
( a in CQC-WFF Al & b in bool (bound_QC-variables Al) & C = [a,b] ) by ZFMISC_1:def 2;
then reconsider K = C `2 as Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t 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. (Al -one_in { u where u is QC-symbol of Al : not x. u 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. (Al -one_in { t where t is QC-symbol of Al : not x. t 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. (Al -one_in { u where u is QC-symbol of Al : not x. u 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. (Al -one_in { t where t is QC-symbol of Al : not x. t 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. (Al -one_in { u where u is QC-symbol of Al : not x. u 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. (Al -one_in { u where u is QC-symbol of Al : not x. u 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))}))] as Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] ;
consider h being Function of NAT,[:(CQC-WFF Al),(bool (bound_QC-variables Al)):] such that
A6: ( h . 0 = A & ( for n being Element of NAT holds S₁[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A5);
set CY = CX \/ { ((h . n) `1) where n is Element of NAT : verum } ;

now :: thesis:

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

now :: thesis:

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

end;

hence a in CQC-WFF Al ; :: thesis:

end;

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

A9: now :: thesis:

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

A18: now :: thesis:

assume A19: a = 0 ; :: thesis:
take y = x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 A6, A19, MCART_1:7;
hence CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A11, A14, A15, A16, A17, Th21; :: thesis:

end;

now :: thesis:

assume a <> 0 ; :: thesis:
then consider m being natural number such that
A20: a = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A21: ex K, L being Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' r9) 'or' ((the_scope_of (f,a)) . ((bound_in (f,a)),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] ) by A6, A20;
set K = (h . m) `2 ;
set L = (still_not-bound_in {r9}) \/ ((h . m) `2);
take y = x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 A21, MCART_1:7;
hence CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A11, A14, A15, A16, A17, Th21; :: thesis:

end;

hence ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A18; :: 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
A22: ( dom F = NAT & ( for a being set st a in NAT holds
F . a = H₁(a) ) ) from FUNCT_1:sch 3();
A23: CY c= union (rng F)

proof

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

A25: now :: thesis:

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

now :: thesis:

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 A28: { ((h . n) `1) where n is Element of NAT : n in 0 } = {} by XBOOLE_0:def 1;
F . 0 in rng F by A22, FUNCT_1:3;
hence a in union (rng F) by A26, A27, A28, TARSKI:def 4; :: thesis:

end;

now :: thesis:

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

end;

hence a in union (rng F) by A24, A25, 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
A32: a in b and
A33: b in rng F by TARSKI:def 4;
consider c being set such that
A34: c in dom F and
A35: F . c = b by A33, FUNCT_1:def 3;
reconsider n = c as Element of NAT by A22, A34;
A36: a in CX \/ { ((h . m) `1) where m is Element of NAT : m in n } by A22, A32, A35;

A37: now :: thesis:

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

end;

now :: thesis:

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 A39: 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 A39; :: thesis:

end;

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

end;

then A40: CY = union (rng F) by A23, XBOOLE_0:def 10;
A41: 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
A42: n < m ; :: thesis:
A43: F . n = CX \/ { ((h . i) `1) where i is Element of NAT : i in n } by A22;
A44: F . m = CX \/ { ((h . i) `1) where i is Element of NAT : i in m } by A22;

now :: thesis:

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

A46: now :: thesis:

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

end;

now :: thesis:

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
A48: (h . i) `1 = a and
A49: i in n ;
i < n by A49, NAT_1:44;
then i < m by A42, XXREAL_0:2;
then i in m by NAT_1:44;
then A50: a in { ((h . j) `1) where j is Element of NAT : j in m } by A48;
{ ((h . j) `1) where j is Element of NAT : j in m } c= F . m by A44, XBOOLE_1:7;
hence a in F . m by A50; :: thesis:

end;

hence a in F . m by A43, A45, A46, XBOOLE_0:def 3; :: thesis:

end;

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

end;

rng F c= bool (CQC-WFF Al)

proof

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

now :: thesis:

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 Al by MCART_1:10; :: thesis:

end;

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

end;

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

proof

let n be Element of NAT ; :: thesis:

now :: thesis:

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
A55: a = (h . j) `1 and
A56: j in n + 1 ;
j < n + 1 by A56, NAT_1:44;
then A57: j + 1 <= n + 1 by NAT_1:13;

A58: now :: thesis:

assume j + 1 = n + 1 ; :: thesis:
then A59: a in {((h . n) `1)} by A55, 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 A59; :: thesis:

end;

now :: thesis:

assume j + 1 <= n ; :: thesis:
then j < n by NAT_1:13;
then j in n by NAT_1:44;
then A60: a in { ((h . k) `1) where k is Element of NAT : k in n } by A55;
{ ((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 A60; :: thesis:

end;

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

end;

then A61: { ((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 :: thesis:

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

A63: now :: thesis:

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
A64: (h . j) `1 = a and
A65: j in n ;
A66: n <= n + 1 by NAT_1:11;
j < n by A65, NAT_1:44;
then j < n + 1 by A66, 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 A64; :: thesis:

end;

now :: thesis:

assume a in {((h . n) `1)} ; :: thesis:
then A67: 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 A67; :: thesis:

end;

hence a in { ((h . i) `1) where i is Element of NAT : i in n + 1 } by A62, A63, 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 A61, 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 A22;
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 A22; :: thesis:

end;

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

proof

A69: (h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))}) by A6, MCART_1:7;
reconsider s = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))) as Element of CQC-WFF Al ;
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 A2;
hence S₂[ 0 ] by A69, Th27; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
assume A71: S₂[k] ; :: thesis:
A72: ex K, L being Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] ) by A6;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of (bound_QC-variables Al) by A71;
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. (Al -one_in { t where t is QC-symbol of Al : not x. t 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))))) is finite by CQC_SIM1:19;
hence S₂[k + 1] by A71, A72, MCART_1:7; :: thesis:

end;

A73: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A68, A70);
defpred S₃[ Element of NAT ] means ( still_not-bound_in (F . ($1 + 1)) c= (h . $1) `2 & not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . ($1 + 1))}) \/ ((h . $1) `2) } ) in still_not-bound_in ((F . ($1 + 1)) \/ {(f . ($1 + 1))}) );
A74: for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {(f . (k + 1))}) \/ ((h . k) `2) } ) in still_not-bound_in ((F . (k + 1)) \/ {(f . (k + 1))}) )

proof

A75: S₃[ 0 ]

proof

set r = ('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } ))));
set A1 = {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))};
reconsider s = f . 1 as Element of CQC-WFF Al ;
A76: (h . 0) `2 = still_not-bound_in (CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))}) by A6, MCART_1:7;
reconsider B = (h . 0) `2 as Subset of (bound_QC-variables Al) by A6, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool (bound_QC-variables Al) ;
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 of Al such that
A77: not x in C by A68, Th28;
consider u being QC-symbol of Al such that
A78: x. u = x by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in C } by A77, A78;
then reconsider A = { t where t is QC-symbol of Al : not x. t in C } as non empty set ;

now :: thesis:

let a be set ; :: thesis:
assume a in A ; :: thesis:
then ex t being QC-symbol of Al st
( a = t & not x. t in C ) ;
hence a in QC-symbols Al ; :: thesis:

end;

then reconsider A = { t where t is QC-symbol of Al : not x. t in C } as non empty Subset of (QC-symbols Al) by TARSKI:def 3;
set u = Al -one_in A;
Al -one_in A = the Element of A by QC_LANG1:def 41;
then Al -one_in A in A ;
then A79: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
A80: F . 0 = CX \/ { ((h . n) `1) where n is Element of NAT : n in 0 } by A22;

now :: thesis:

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 A81: { ((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. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))) by A6, MCART_1:7;
then F . (0 + 1) = CX \/ {(('not' (f . 0)) 'or' ((the_scope_of (f,0)) . ((bound_in (f,0)),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {(f . 0)}) } )))))} by A54, A80, A81;
hence S₃[ 0 ] by A76, A79, Th27; :: thesis:

end;

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

proof

let k be Element of NAT ; :: thesis:
assume A83: S₃[k] ; :: thesis:
reconsider s = f . (k + 2) as Element of CQC-WFF Al ;
A84: ex K, L being Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] ) by A6;
set K = (h . k) `2 ;
reconsider K = (h . k) `2 as Subset of (bound_QC-variables Al) by A73;
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. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } ))));
A85: (h . (k + 1)) `1 = ('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))) by A84, MCART_1:7;
A86: (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. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))) by A84, MCART_1:7;
reconsider B = (h . (k + 1)) `2 as Subset of (bound_QC-variables Al) by A84, MCART_1:7;
reconsider C = (still_not-bound_in {s}) \/ B as Element of bool (bound_QC-variables Al) ;
still_not-bound_in s is finite by CQC_SIM1:19;
then A87: still_not-bound_in {s} is finite by Th26;
(h . (k + 1)) `2 is finite by A73;
then consider x being bound_QC-variable of Al such that
A88: not x in C by A87, Th28;
consider u being QC-symbol of Al such that
A89: x. u = x by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B } by A88, A89;
then reconsider A = { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B } as non empty set ;

now :: thesis:

let a be set ; :: thesis:
assume a in A ; :: thesis:
then ex t being QC-symbol of Al st
( a = t & not x. t in C ) ;
hence a in QC-symbols Al ; :: thesis:

end;

then reconsider A = { t where t is QC-symbol of Al : not x. t in (still_not-bound_in {s}) \/ B } as non empty Subset of (QC-symbols Al) by TARSKI:def 3;
set u = Al -one_in A;
Al -one_in A = the Element of A by QC_LANG1:def 41;
then Al -one_in A in A ;
then A90: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
then A91: not x. (Al -one_in A) in still_not-bound_in {s} by XBOOLE_0:def 3;
(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. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))) c= B by A83, A86, XBOOLE_1:9;
then (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. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))}) c= B by Th26;
then A92: still_not-bound_in ((F . (k + 1)) \/ {(('not' (f . (k + 1))) 'or' ((the_scope_of (f,(k + 1))) . ((bound_in (f,(k + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in K \/ (still_not-bound_in {(f . (k + 1))}) } )))))}) c= B by Th27;
then still_not-bound_in (F . ((k + 1) + 1)) c= B by A54, A85;
then not x. (Al -one_in A) in still_not-bound_in (F . ((k + 1) + 1)) by A90, XBOOLE_0:def 3;
then not x. (Al -one_in A) in (still_not-bound_in (F . ((k + 1) + 1))) \/ (still_not-bound_in {s}) by A91, XBOOLE_0:def 3;
hence S₃[k + 1] by A54, A85, A92, Th27; :: thesis:

end;

for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A75, A82);
hence for k being Element of NAT holds
( still_not-bound_in (F . (k + 1)) c= (h . k) `2 & not x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 :: thesis:

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 A93: F . 0 = CX \/ {} by A22;
then A94: S₄[ 0 ] ;
A95: for k being Element of NAT st S₄[k] holds
S₄[k + 1]

proof

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

now :: thesis:

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

A100: now :: thesis:

now :: thesis:

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

end;

then reconsider A = { t where t is QC-symbol of Al : not x. t in still_not-bound_in (CX \/ {r1}) } as non empty Subset of (QC-symbols Al) by TARSKI:def 3;
set u = Al -one_in A;
Al -one_in A = the Element of A by QC_LANG1:def 41;
then Al -one_in A in A ;
then consider t being QC-symbol of Al such that
A109: t = Al -one_in A and
A110: not x. t in still_not-bound_in (CX \/ {r1}) ;
A111: not x. t in (still_not-bound_in CX) \/ (still_not-bound_in {r1}) by A110, Th27;
then A112: not x. t in still_not-bound_in {r1} by XBOOLE_0:def 3;
A113: F . 0 = CX \/ { ((h . n) `1) where n is Element of NAT : n in 0 } by A22;

now :: thesis:

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;

end;

now :: thesis:

assume k <> 0 ; :: thesis:
then consider k1 being natural number such that
A121: k = k1 + 1 by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
A122: ex K, L being Subset of (bound_QC-variables Al) 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. (Al -one_in { t where t is QC-symbol of Al : not x. t in L } ))))),(K \/ (still_not-bound_in (('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { u where u is QC-symbol of Al : not x. u in L } )))))))] ) by A6;
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. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))));
A123: r = ('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))) by A121, A122, MCART_1:7;
reconsider s = (the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ))) as Element of CQC-WFF Al ;
A124: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*> by A99, A121, 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 Al))*> by A98, Th25;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then |- ((f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*r*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then A125: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' (VERUM Al))*> by A123, A124, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A126: |- (f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 Al))*> by A98, Th25;
then |- ((f1 ^ <*s*>) ^ <*(Suc (f1 ^ <*r*>))*>) ^ <*('not' (VERUM Al))*> by CALCUL_1:5;
then |- ((f1 ^ <*s*>) ^ <*(('not' (f . (k1 + 1))) 'or' ((the_scope_of (f,(k1 + 1))) . ((bound_in (f,(k1 + 1))),(x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } )))))*>) ^ <*('not' (VERUM Al))*> by A123, CALCUL_1:5;
then A127: |- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*> by A126, CALCUL_2:24;
set y = x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } );
set u = Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ;
reconsider r2 = the_scope_of (f,(k1 + 1)) as Element of CQC-WFF Al ;
reconsider y2 = bound_in (f,(k1 + 1)) as bound_QC-variable of Al ;
reconsider r1 = f . (k1 + 1) as Element of CQC-WFF Al ;
r1 in ExCl Al by A3, A4, FUNCT_1:3;
then consider y1 being bound_QC-variable of Al, s1 being Element of CQC-WFF Al such that
A128: r1 = Ex (y1,s1) by Def3;
A129: s1 = Ex-the_scope_of r1 by A128, Th22;
A130: r2 = Ex-the_scope_of r1 by Def7;
A131: y1 = Ex-bound_in r1 by A128, Th22;
A132: y2 = Ex-bound_in r1 by Def6;
reconsider Z = F . k as Subset of (CQC-WFF Al) ;
not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (Z \/ {r1}) by A74, A121;
then A133: not x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 A134: not x. (Al -one_in { t where t is QC-symbol of Al : not x. t 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 A97, Th29;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (rng f1) by A133, XBOOLE_0:def 3;
then A135: not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in f1 by Th30;
not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in r1 by A134, Th26;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*r1*> by CALCUL_1:60;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in f1) \/ (still_not-bound_in <*r1*>) by A135, XBOOLE_0:def 3;
then A136: not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in (f1 ^ <*r1*>) by CALCUL_1:59;
still_not-bound_in (VERUM Al) = {} by QC_LANG3:3;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ('not' (VERUM Al)) by QC_LANG3:7;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in <*('not' (VERUM Al))*> by CALCUL_1:60;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in (still_not-bound_in (f1 ^ <*r1*>)) \/ (still_not-bound_in <*('not' (VERUM Al))*>) by A136, XBOOLE_0:def 3;
then not x. (Al -one_in { t where t is QC-symbol of Al : not x. t in ((h . k1) `2) \/ (still_not-bound_in {(f . (k1 + 1))}) } ) in still_not-bound_in ((f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*>) by CALCUL_1:59;
then |- (f1 ^ <*r1*>) ^ <*('not' (VERUM Al))*> by A127, A128, A129, A130, A131, A132, CALCUL_1:61;
then |- f1 ^ <*('not' (VERUM Al))*> by A125, CALCUL_2:26;
then F . k |- 'not' (VERUM Al) by A97, HENMODEL:def 1;
hence contradiction by A96, Th24; :: thesis:

end;

hence contradiction by A100; :: thesis:

end;

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

end;

for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A94, A95);
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 A41;
then reconsider CY = CY as Consistent Subset of (CQC-WFF Al) by A40, HENMODEL:11;
take CY ; :: thesis:
thus ( CX c= CY & CY is with_examples ) by A9, Def2, XBOOLE_1:7; :: thesis: