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

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

end;

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

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

end;

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

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

end;

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

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

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

end;

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

end;

thus for q, r being Element of CQC-WFF A
for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) :: thesis:

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

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

end;

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

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

end;

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

end;

thus for q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for t being QC-symbol of A
for K being Element of Fin (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X :: thesis:

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

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

end;

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

end;

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