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 sequence of (CQC-WFF Al) by A3, A4, FUNCT_2:2;
defpred S₁[ 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 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 Nat; :: thesis:
let C be Element of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):]; :: thesis:
set K = C `2 ;
ex a, b being object 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) ;
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 sequence of [:(CQC-WFF Al),(bool (bound_QC-variables Al)):] such that
A6: ( h . 0 = A & ( for n being Nat holds S₁[n,h . n,h . (n + 1)] ) ) from RECDEF_1:sch 2(A5);
set CY = CX \/ { ((h . n) `1) where n is Nat : verum } ;

now :: thesis:

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

now :: thesis:

assume not a in CX ; :: thesis:
then a in { ((h . n) `1) where n is Nat : verum } by A7, XBOOLE_0:def 3;
then consider n being Nat such that
A8: a = (h . n) `1 ;
ex c, d being object 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; :: thesis:

end;

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

end;

then reconsider CY = CX \/ { ((h . n) `1) where n is 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 object such that
A10: a in dom f and
A11: f . a = Ex (x,p) by A4, FUNCT_1:def 3;
reconsider a = a as 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 Nat : verum } ;
A17: { ((h . n) `1) where n is Nat : verum } c= CY by XBOOLE_1:7;
A18: ( a = 0 implies ex y being bound_QC-variable of Al st CY |- ('not' (Ex (x,p))) 'or' (p . (x,y)) ) by A6, A11, A14, A15, A16, A17, Th21;

now :: thesis:

assume a <> 0 ; :: thesis:
then consider m being Nat such that
A20: a = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
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;
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 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 5();
A23: CY c= union (rng F)

proof

let a be object ; :: 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 Nat : n in 0 } by A22;

now :: thesis:

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

end;

then A28: { ((h . n) `1) where n is 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 Nat : verum } ; :: thesis:
then consider n being Nat such that
A29: a = (h . n) `1 ;
n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
then A30: a in { ((h . m) `1) where m is Nat : m in n + 1 } by A29;
F . (n + 1) = CX \/ { ((h . m) `1) where m is Nat : m in n + 1 } by A22;
then A31: { ((h . m) `1) where m is 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 object ; :: 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 object 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 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 Nat : m in n } ; :: thesis:
then ex m being Nat st
( a = (h . m) `1 & m in n ) ;
then A39: a in { ((h . i) `1) where i is Nat : verum } ;
{ ((h . i) `1) where i is 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;
A41: for n, m being Nat st m in dom F & n in dom F & n < m holds
F . n c= F . m

proof

let n, m be Nat; :: thesis:
assume that
m in dom F and
n in dom F and
A42: n < m ; :: thesis:
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;
A43: F . n = CX \/ { ((h . i) `1) where i is Nat : i in n } by A22;
A44: F . m = CX \/ { ((h . i) `1) where i is Nat : i in m } by A22;

now :: thesis:

let a be object ; :: 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 Nat : i in n } ; :: thesis:
then consider i being Nat such that
A48: (h . i) `1 = a and
A49: i in Segm n ;
i < n by A49, NAT_1:44;
then i < m by A42, XXREAL_0:2;
then i in Segm m by NAT_1:44;
then A50: a in { ((h . j) `1) where j is Nat : j in m } by A48;
{ ((h . j) `1) where j is 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 ; :: thesis:

end;

rng F c= bool (CQC-WFF Al)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then consider b being object 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 Nat : i in b } by A22;

now :: thesis:

let c be object ; :: thesis:
assume c in { ((h . i) `1) where i is Nat : i in b } ; :: thesis:
then ex i being 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 Nat : i in b } c= CQC-WFF Al ;
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 sequence of (bool (CQC-WFF Al)) by A22, FUNCT_2:2;
A54: for n being Nat holds F . (n + 1) = (F . n) \/ {((h . n) `1)}

proof

let n be Nat; :: thesis:
A55: n in NAT by ORDINAL1:def 12;

now :: thesis:

let a be object ; :: thesis:
assume a in { ((h . i) `1) where i is Nat : i in n + 1 } ; :: thesis:
then consider j being Nat such that
A56: a = (h . j) `1 and
A57: j in Segm (n + 1) ;
j < n + 1 by A57, NAT_1:44;
then A58: j + 1 <= n + 1 by NAT_1:13;

A59: now :: thesis:

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

end;

now :: thesis:

assume j + 1 <= n ; :: thesis:
then j < n by NAT_1:13;
then j in Segm n by NAT_1:44;
then A61: a in { ((h . k) `1) where k is Nat : k in n } by A56;
{ ((h . k) `1) where k is Nat : k in n } c= { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} by XBOOLE_1:7;
hence a in { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} by A61; :: thesis:

end;

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

end;

then A62: { ((h . k) `1) where k is Nat : k in n + 1 } c= { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} ;

now :: thesis:

let a be object ; :: thesis:
assume A63: a in { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} ; :: thesis:

A64: now :: thesis:

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

end;

now :: thesis:

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

end;

hence a in { ((h . i) `1) where i is Nat : i in n + 1 } by A63, A64, XBOOLE_0:def 3; :: thesis:

end;

then { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} c= { ((h . k) `1) where k is Nat : k in n + 1 } ;
then { ((h . i) `1) where i is Nat : i in n } \/ {((h . n) `1)} = { ((h . k) `1) where k is Nat : k in n + 1 } by A62;
then F . (n + 1) = CX \/ ( { ((h . k) `1) where k is Nat : k in n } \/ {((h . n) `1)}) by A22;
then F . (n + 1) = H₁(n) \/ {((h . n) `1)} by XBOOLE_1:4;
hence F . (n + 1) = (F . n) \/ {((h . n) `1)} by A22, A55; :: thesis:

end;

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

proof

A70: (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;
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 A70, Th27; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A72: S₂[k] ; :: thesis:
A73: 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 A72;
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 A72, A73; :: thesis:

end;

A74: for k being Nat holds S₂[k] from NAT_1:sch 2(A69, A71);
defpred S₃[ 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))}) );
A75: for k being 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

A76: 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 ;
A77: (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;
reconsider B = (h . 0) `2 as Subset of (bound_QC-variables Al) by A6;
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
A78: not x in C by A69, Th28;
consider u being QC-symbol of Al such that
A79: x. u = x by QC_LANG3:30;
u in { t where t is QC-symbol of Al : not x. t in C } by A78, A79;
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 object ; :: 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 A80: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
A81: F . 0 = CX \/ { ((h . n) `1) where n is Nat : n in 0 } by A22;

now :: thesis:

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

end;

then A82: { ((h . n) `1) where n is 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;
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, A81, A82;
hence S₃[ 0 ] by A77, A80, Th27; :: thesis:

end;

A83: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume A84: S₃[k] ; :: thesis:
reconsider s = f . (k + 2) as Element of CQC-WFF Al ;
A85: 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 A74;
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))}) } ))));
A86: (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 A85;
A87: (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 A85;
reconsider B = (h . (k + 1)) `2 as Subset of (bound_QC-variables Al) by A85;
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 A88: still_not-bound_in {s} is finite by Th26;
(h . (k + 1)) `2 is finite by A74;
then consider x being bound_QC-variable of Al such that
A89: not x in C by A88, Th28;
consider u being QC-symbol of Al such that
A90: 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 A89, A90;
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 object ; :: 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 A91: ex t being QC-symbol of Al st
( t = Al -one_in A & not x. t in C ) ;
then A92: 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 A84, A87, 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 A93: 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, A86;
then not x. (Al -one_in A) in still_not-bound_in (F . ((k + 1) + 1)) by A91, 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 A92, XBOOLE_0:def 3;
hence S₃[k + 1] by A54, A86, A93, Th27; :: thesis:

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(A76, A83);
hence for k being 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₄[ Nat] means F . $1 is Consistent ;

now :: thesis:

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

end;

then { ((h . i) `1) where i is Nat : i in 0 } = {} by XBOOLE_0:def 1;
then A94: F . 0 = CX \/ {} by A22;
then A95: S₄[ 0 ] ;
A96: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis:
assume A97: S₄[k] ; :: thesis:
ex c, d being object 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 ;

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
A98: rng f1 c= F . k and
A99: |- (f1 ^ <*r*>) ^ <*('not' (VERUM Al))*> by HENMODEL:8;
A100: |- (f1 ^ <*('not' (f . k))*>) ^ <*('not' (f . k))*> by CALCUL_2:21;

A101: now :: thesis:

now :: thesis:

let a be object ; :: 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
A110: t = Al -one_in A and
A111: not x. t in still_not-bound_in (CX \/ {r1}) ;
A112: not x. t in (still_not-bound_in CX) \/ (still_not-bound_in {r1}) by A111, Th27;
then A113: not x. t in still_not-bound_in {r1} by XBOOLE_0:def 3;
A114: F . 0 = CX \/ { ((h . n) `1) where n is Nat : n in 0 } by A22;

now :: thesis:

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

end;

end;

now :: thesis:

assume k <> 0 ; :: thesis:
then consider k1 being Nat such that
A122: k = k1 + 1 by NAT_1:6;
reconsider k1 = k1 as Nat ;
A123: 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))}) } ))));
A124: 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 A122, A123;
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 ;
A125: |- (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 A100, A122, 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 A99, 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 A126: |- (f1 ^ <*('not' (f . (k1 + 1)))*>) ^ <*('not' (VERUM Al))*> by A124, A125, CALCUL_2:24;
|- (f1 ^ <*s*>) ^ <*s*> by CALCUL_2:21;
then A127: |- (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 A99, 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 A124, CALCUL_1:5;
then A128: |- (f1 ^ <*s*>) ^ <*('not' (VERUM Al))*> by A127, 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
A129: r1 = Ex (y1,s1) by Def3;
A130: s1 = Ex-the_scope_of r1 by A129, Th22;
A131: r2 = Ex-the_scope_of r1 by Def7;
A132: y1 = Ex-bound_in r1 by A129, Th22;
A133: 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 A75, A122;
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 Z) \/ (still_not-bound_in {r1}) by Th27;
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 {r1} by XBOOLE_0:def 3;
still_not-bound_in (rng f1) c= still_not-bound_in Z by A98, 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 A134, 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 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 A135, 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 A136, XBOOLE_0:def 3;
then A137: 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 A137, 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 A128, A129, A130, A131, A132, A133, CALCUL_1:61;
then |- f1 ^ <*('not' (VERUM Al))*> by A126, CALCUL_2:26;
then F . k |- 'not' (VERUM Al) by A98, HENMODEL:def 1;
hence contradiction by A97, Th24; :: thesis:

end;

hence contradiction by A101; :: thesis:

end;

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

end;

for n being Nat holds S₄[n] from NAT_1:sch 2(A95, A96);
then for n, m being 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, XBOOLE_1:7; :: thesis: