set S = [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):];
set A = { X where X is Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] : X is_Sep-closed_on p } ;
{ X where X is Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] : X is_Sep-closed_on p } c= bool [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):]

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { X where X is Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] : X is_Sep-closed_on p } ; :: thesis:
then ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = a & X is_Sep-closed_on p ) ;
hence a in bool [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ; :: thesis:

end;

then reconsider A = { X where X is Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] : X is_Sep-closed_on p } as Subset-Family of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ;
take X = meet A; :: thesis:
set B = [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):];
[#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] is_Sep-closed_on p

proof

thus [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] by MCART_1:80; :: according to CQC_SIM1:def 11 :: thesis:
thus for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [('not' q),k,K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] holds
[q,k,K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] by MCART_1:80; :: thesis:
thus for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [(q '&' r),k,K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] holds
( [q,k,K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] & [r,(k + (QuantNbr q)),K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ) by MCART_1:80; :: thesis:
let q be Element of CQC-WFF ; :: thesis:
let x be Element of bound_QC-variables ; :: thesis:
let k be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume [(All (x,q)),k,K,f] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ; :: thesis:
A1: rng (f +* (x .--> (x. k))) c= (rng f) \/ (rng (x .--> (x. k))) by FUNCT_4:17;
A2: rng (x .--> (x. k)) = {(x. k)} by FUNCOP_1:8;
A3: bound_QC-variables \/ {(x. k)} = bound_QC-variables by ZFMISC_1:40;
rng f c= bound_QC-variables by RELAT_1:def 19;
then (rng f) \/ (rng (x .--> (x. k))) c= bound_QC-variables by A2, A3, XBOOLE_1:9;
then A4: rng (f +* (x .--> (x. k))) c= bound_QC-variables by A1, XBOOLE_1:1;
dom (f +* (x .--> (x. k))) = (dom f) \/ (dom (x .--> (x. k))) by FUNCT_4:def 1
.= bound_QC-variables \/ (dom (x .--> (x. k))) by FUNCT_2:def 1
.= bound_QC-variables \/ {x} by FUNCOP_1:13
.= bound_QC-variables by ZFMISC_1:40 ;
then f +* (x .--> (x. k)) is Function of bound_QC-variables,bound_QC-variables by A4, FUNCT_2:def 1, RELSET_1:4;
then reconsider ff = f +* (x .--> (x. k)) as Element of Funcs (bound_QC-variables,bound_QC-variables) by FUNCT_2:8;
[q,(k + 1),(K \/ {.x.}),ff] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] by MCART_1:80;
hence [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ; :: thesis:

end;

then A5: [#] [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] in A ;
for Y being set st Y in A holds
[p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in Y

proof

let Y be set ; :: thesis:
assume Y in A ; :: thesis:
then ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = Y & X is_Sep-closed_on p ) ;
hence [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in Y by Def12; :: thesis:

end;

hence [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in X by A5, SETFAM_1:def 1; :: according to CQC_SIM1:def 11 :: thesis:
thus for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [('not' q),k,K,f] in X holds
[q,k,K,f] in X :: thesis:

proof

let q be Element of CQC-WFF ; :: thesis:
let k be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A6: [('not' q),k,K,f] in X ; :: thesis:
for Y being set st Y in A holds
[q,k,K,f] in Y

proof

let Y be set ; :: thesis:
assume A7: Y in A ; :: thesis:
then A8: ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = Y & X is_Sep-closed_on p ) ;
[('not' q),k,K,f] in Y by A6, A7, SETFAM_1:def 1;
hence [q,k,K,f] in Y by A8, Def12; :: thesis:

end;

hence [q,k,K,f] in X by A5, SETFAM_1:def 1; :: thesis:

end;

thus for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) :: thesis:

proof

let q, r be Element of CQC-WFF ; :: thesis:
let k be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A9: [(q '&' r),k,K,f] in X ; :: thesis:
for Y being set st Y in A holds
[q,k,K,f] in Y

proof

let Y be set ; :: thesis:
assume A10: Y in A ; :: thesis:
then A11: ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = Y & X is_Sep-closed_on p ) ;
[(q '&' r),k,K,f] in Y by A9, A10, SETFAM_1:def 1;
hence [q,k,K,f] in Y by A11, Def12; :: thesis:

end;

hence [q,k,K,f] in X by A5, SETFAM_1:def 1; :: thesis:
for Y being set st Y in A holds
[r,(k + (QuantNbr q)),K,f] in Y

proof

let Y be set ; :: thesis:
assume A12: Y in A ; :: thesis:
then A13: ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = Y & X is_Sep-closed_on p ) ;
[(q '&' r),k,K,f] in Y by A9, A12, SETFAM_1:def 1;
hence [r,(k + (QuantNbr q)),K,f] in Y by A13, Def12; :: thesis:

end;

hence [r,(k + (QuantNbr q)),K,f] in X by A5, SETFAM_1:def 1; :: thesis:

end;

thus for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [(All (x,q)),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X :: thesis:

proof

let q be Element of CQC-WFF ; :: thesis:
let x be Element of bound_QC-variables ; :: thesis:
let k be Element of NAT ; :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A14: [(All (x,q)),k,K,f] in X ; :: thesis:
for Y being set st Y in A holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y

proof

let Y be set ; :: thesis:
assume A15: Y in A ; :: thesis:
then A16: ex X being Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] st
( X = Y & X is_Sep-closed_on p ) ;
[(All (x,q)),k,K,f] in Y by A14, A15, SETFAM_1:def 1;
hence [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y by A16, Def12; :: thesis:

end;

hence [q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in X by A5, SETFAM_1:def 1; :: thesis:

end;

let D be Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):]; :: thesis:
assume D is_Sep-closed_on p ; :: thesis:
then D in A ;
hence X c= D by SETFAM_1:3; :: thesis: