let q, p be Element of CQC-WFF ; :: thesis:
let k be Element of NAT ; :: thesis:
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
let K be Finite_Subset of bound_QC-variables; :: thesis:
assume that
A1: [q,k,K,f] in SepQuadruples p and
A2: [q,k,K,f] <> [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] and
A3: not [('not' q),k,K,f] in SepQuadruples p and
A4: for r being Element of CQC-WFF holds not [(q '&' r),k,K,f] in SepQuadruples p and
A5: for r being Element of CQC-WFF
for l being Element of NAT holds
( not k = l + (QuantNbr r) or not [(r '&' q),l,K,f] in SepQuadruples p ) and
A6: for x being Element of bound_QC-variables
for l being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds
( not l + 1 = k or not h +* ({x} --> (x. l)) = f or ( not [(All (x,q)),l,K,h] in SepQuadruples p & not [(All (x,q)),l,(K \ {x}),h] in SepQuadruples p ) ) ; :: thesis:
reconsider Y = (SepQuadruples p) \ {[q,k,K,f]} as Subset of [:CQC-WFF,NAT,(Fin bound_QC-variables),(Funcs (bound_QC-variables,bound_QC-variables)):] ;
A7: SepQuadruples p is_Sep-closed_on p by Def13;
A8: 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 Y holds
[q,k,K,f] in Y

let s be Element of CQC-WFF ; :: thesis:
let l be Element of NAT ; :: thesis:
let L be Finite_Subset of bound_QC-variables; :: thesis:
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A9: [('not' s),l,L,h] in Y ; :: thesis:
then ( s <> q or l <> k or L <> K or f <> h ) by A3, XBOOLE_0:def 5;
then A10: [s,l,L,h] <> [q,k,K,f] by MCART_1:29;
[('not' s),l,L,h] in SepQuadruples p by A9, XBOOLE_0:def 5;
then [s,l,L,h] in SepQuadruples p by A7, Def12;
hence [s,l,L,h] in Y by A10, ZFMISC_1:56; :: thesis:

end;

A11: 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 Y holds
( [q,k,K,f] in Y & [r,(k + (QuantNbr q)),K,f] in Y )

let s, r be Element of CQC-WFF ; :: thesis:
let l be Element of NAT ; :: thesis:
let L be Finite_Subset of bound_QC-variables; :: thesis:
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume [(s '&' r),l,L,h] in Y ; :: thesis:
then A12: [(s '&' r),l,L,h] in SepQuadruples p by XBOOLE_0:def 5;
then ( s <> q or l <> k or L <> K or f <> h ) by A4;
then A13: [s,l,L,h] <> [q,k,K,f] by MCART_1:29;
[s,l,L,h] in SepQuadruples p by A7, A12, Def12;
hence [s,l,L,h] in Y by A13, ZFMISC_1:56; :: thesis:
( r <> q or L <> K or f <> h or l + (QuantNbr s) <> k ) by A5, A12;
then A14: [r,(l + (QuantNbr s)),L,h] <> [q,k,K,f] by MCART_1:29;
[r,(l + (QuantNbr s)),L,h] in SepQuadruples p by A7, A12, Def12;
hence [r,(l + (QuantNbr s)),L,h] in Y by A14, ZFMISC_1:56; :: thesis:

end;

A15: Y c= SepQuadruples p by XBOOLE_1:36;
A16: 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 Y holds
[q,(k + 1),(K \/ {x}),(f +* (x .--> (x. k)))] in Y

let s be Element of CQC-WFF ; :: thesis:
let x be Element of bound_QC-variables ; :: thesis:
let l be Element of NAT ; :: thesis:
let L be Finite_Subset of bound_QC-variables; :: thesis:
let h be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis:
assume A17: [(All (x,s)),l,L,h] in Y ; :: thesis:

assume that
A18: not [(All (x,q)),l,K,h] in SepQuadruples p and
A19: not [(All (x,q)),l,(K \ {x}),h] in SepQuadruples p ; :: thesis:
A20: ( s <> q or ( L <> K & L <> K \ {x} ) ) by A17, A18, A19, XBOOLE_0:def 5;
assume A21: s = q ; :: thesis:
A22: ( x in L or not x in L ) ;
assume A23: L \/ {x} = K ; :: thesis:
then K \ {x} = L \ {x} by XBOOLE_1:40;
hence contradiction by A20, A21, A23, A22, ZFMISC_1:40, ZFMISC_1:57; :: thesis:

end;

then ( s <> q or l + 1 <> k or L \/ {x} <> K or f <> h +* ({x} --> (x. l)) ) by A6;
then A24: [s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] <> [q,k,K,f] by MCART_1:29;
[(All (x,s)),l,L,h] in SepQuadruples p by A17, XBOOLE_0:def 5;
then [s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in SepQuadruples p by A7, Def12;
hence [s,(l + 1),(L \/ {x}),(h +* (x .--> (x. l)))] in Y by A24, ZFMISC_1:56; :: thesis:

end;

[p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in SepQuadruples p by A7, Def12;
then [p,(index p),({}. bound_QC-variables),(id bound_QC-variables)] in Y by A2, ZFMISC_1:56;
then Y is_Sep-closed_on p by A8, A11, A16, Def12;
then SepQuadruples p c= Y by Def13;
then Y = SepQuadruples p by A15, XBOOLE_0:def 10;
hence contradiction by A1, ZFMISC_1:57; :: thesis: