let A be QC-alphabet ; :: thesis: for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let t be QC-symbol of A; :: thesis: for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let p, q be Element of CQC-WFF A; :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let K be Element of Fin (bound_QC-variables A); :: thesis: ( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

assume that

A1: [q,t,K,f] in SepQuadruples p and

A2: [q,t,K,f] <> [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] and

A3: not [('not' q),t,K,f] in SepQuadruples p and

A4: for r being Element of CQC-WFF A holds not [(q '&' r),t,K,f] in SepQuadruples p and

A5: for r being Element of CQC-WFF A

for u being QC-symbol of A holds

( not t = u + (QuantNbr r) or not [(r '&' q),u,K,f] in SepQuadruples p ) and

A6: for x being Element of bound_QC-variables A

for u being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds

( not u ++ = t or not h +* ({x} --> (x. u)) = f or ( not [(All (x,q)),u,K,h] in SepQuadruples p & not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) ; :: thesis: contradiction

reconsider Y = (SepQuadruples p) \ {[q,t,K,f]} as Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] ;

A7: SepQuadruples p is_Sep-closed_on p by Def13;

A8: 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 Y holds

[q,t,K,f] in Y

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 Y holds

( [q,t,K,f] in Y & [r,(t + (QuantNbr q)),K,f] in Y )

A16: 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 Y holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

then [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in Y by A2, ZFMISC_1:56;

then Y is_Sep-closed_on p by A8, A11, A16;

then SepQuadruples p c= Y by Def13;

then Y = SepQuadruples p by A15;

hence contradiction by A1, ZFMISC_1:57; :: thesis: verum

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let t be QC-symbol of A; :: thesis: for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let p, q be Element of CQC-WFF A; :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

let K be Element of Fin (bound_QC-variables A); :: thesis: ( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

assume that

A1: [q,t,K,f] in SepQuadruples p and

A2: [q,t,K,f] <> [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] and

A3: not [('not' q),t,K,f] in SepQuadruples p and

A4: for r being Element of CQC-WFF A holds not [(q '&' r),t,K,f] in SepQuadruples p and

A5: for r being Element of CQC-WFF A

for u being QC-symbol of A holds

( not t = u + (QuantNbr r) or not [(r '&' q),u,K,f] in SepQuadruples p ) and

A6: for x being Element of bound_QC-variables A

for u being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds

( not u ++ = t or not h +* ({x} --> (x. u)) = f or ( not [(All (x,q)),u,K,h] in SepQuadruples p & not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) ; :: thesis: contradiction

reconsider Y = (SepQuadruples p) \ {[q,t,K,f]} as Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] ;

A7: SepQuadruples p is_Sep-closed_on p by Def13;

A8: 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 Y holds

[q,t,K,f] in Y

proof

A11:
for q, r being Element of CQC-WFF A
let s be Element of CQC-WFF A; :: thesis: 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' s),t,K,f] in Y holds

[s,t,K,f] in Y

let u be QC-symbol of A; :: thesis: 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' s),u,K,f] in Y holds

[s,u,K,f] in Y

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' s),u,L,f] in Y holds

[s,u,L,f] in Y

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [('not' s),u,L,h] in Y implies [s,u,L,h] in Y )

assume A9: [('not' s),u,L,h] in Y ; :: thesis: [s,u,L,h] in Y

then ( s <> q or u <> t or L <> K or f <> h ) by A3, XBOOLE_0:def 5;

then A10: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;

[('not' s),u,L,h] in SepQuadruples p by A9, XBOOLE_0:def 5;

then [s,u,L,h] in SepQuadruples p by A7;

hence [s,u,L,h] in Y by A10, ZFMISC_1:56; :: thesis: verum

end;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' s),t,K,f] in Y holds

[s,t,K,f] in Y

let u be QC-symbol of A; :: thesis: 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' s),u,K,f] in Y holds

[s,u,K,f] in Y

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' s),u,L,f] in Y holds

[s,u,L,f] in Y

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [('not' s),u,L,h] in Y implies [s,u,L,h] in Y )

assume A9: [('not' s),u,L,h] in Y ; :: thesis: [s,u,L,h] in Y

then ( s <> q or u <> t or L <> K or f <> h ) by A3, XBOOLE_0:def 5;

then A10: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;

[('not' s),u,L,h] in SepQuadruples p by A9, XBOOLE_0:def 5;

then [s,u,L,h] in SepQuadruples p by A7;

hence [s,u,L,h] in Y by A10, ZFMISC_1:56; :: thesis: verum

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 Y holds

( [q,t,K,f] in Y & [r,(t + (QuantNbr q)),K,f] in Y )

proof

A15:
Y c= SepQuadruples p
by XBOOLE_1:36;
let s, r be Element of CQC-WFF A; :: thesis: 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 [(s '&' r),t,K,f] in Y holds

( [s,t,K,f] in Y & [r,(t + (QuantNbr s)),K,f] in Y )

let u be QC-symbol of A; :: thesis: 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 [(s '&' r),u,K,f] in Y holds

( [s,u,K,f] in Y & [r,(u + (QuantNbr s)),K,f] in Y )

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(s '&' r),u,L,f] in Y holds

( [s,u,L,f] in Y & [r,(u + (QuantNbr s)),L,f] in Y )

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(s '&' r),u,L,h] in Y implies ( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y ) )

assume [(s '&' r),u,L,h] in Y ; :: thesis: ( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y )

then A12: [(s '&' r),u,L,h] in SepQuadruples p by XBOOLE_0:def 5;

then ( s <> q or u <> t or L <> K or f <> h ) by A4;

then A13: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;

[s,u,L,h] in SepQuadruples p by A7, A12;

hence [s,u,L,h] in Y by A13, ZFMISC_1:56; :: thesis: [r,(u + (QuantNbr s)),L,h] in Y

( r <> q or L <> K or f <> h or u + (QuantNbr s) <> t ) by A5, A12;

then A14: [r,(u + (QuantNbr s)),L,h] <> [q,t,K,f] by XTUPLE_0:5;

[r,(u + (QuantNbr s)),L,h] in SepQuadruples p by A7, A12;

hence [r,(u + (QuantNbr s)),L,h] in Y by A14, ZFMISC_1:56; :: thesis: verum

end;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 [(s '&' r),t,K,f] in Y holds

( [s,t,K,f] in Y & [r,(t + (QuantNbr s)),K,f] in Y )

let u be QC-symbol of A; :: thesis: 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 [(s '&' r),u,K,f] in Y holds

( [s,u,K,f] in Y & [r,(u + (QuantNbr s)),K,f] in Y )

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(s '&' r),u,L,f] in Y holds

( [s,u,L,f] in Y & [r,(u + (QuantNbr s)),L,f] in Y )

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(s '&' r),u,L,h] in Y implies ( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y ) )

assume [(s '&' r),u,L,h] in Y ; :: thesis: ( [s,u,L,h] in Y & [r,(u + (QuantNbr s)),L,h] in Y )

then A12: [(s '&' r),u,L,h] in SepQuadruples p by XBOOLE_0:def 5;

then ( s <> q or u <> t or L <> K or f <> h ) by A4;

then A13: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;

[s,u,L,h] in SepQuadruples p by A7, A12;

hence [s,u,L,h] in Y by A13, ZFMISC_1:56; :: thesis: [r,(u + (QuantNbr s)),L,h] in Y

( r <> q or L <> K or f <> h or u + (QuantNbr s) <> t ) by A5, A12;

then A14: [r,(u + (QuantNbr s)),L,h] <> [q,t,K,f] by XTUPLE_0:5;

[r,(u + (QuantNbr s)),L,h] in SepQuadruples p by A7, A12;

hence [r,(u + (QuantNbr s)),L,h] in Y by A14, ZFMISC_1:56; :: thesis: verum

A16: 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 Y holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

proof

[p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in SepQuadruples p
by A7;
let s be Element of CQC-WFF A; :: thesis: 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,s)),t,K,f] in Y holds

[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

let x be Element of bound_QC-variables A; :: thesis: 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,s)),t,K,f] in Y holds

[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

let u be QC-symbol of A; :: thesis: 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,s)),u,K,f] in Y holds

[s,(u ++),(K \/ {x}),(f +* (x .--> (x. u)))] in Y

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,s)),u,L,f] in Y holds

[s,(u ++),(L \/ {x}),(f +* (x .--> (x. u)))] in Y

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,s)),u,L,h] in Y implies [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y )

assume A17: [(All (x,s)),u,L,h] in Y ; :: thesis: [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y

then A23: [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] <> [q,t,K,f] by XTUPLE_0:5;

[(All (x,s)),u,L,h] in SepQuadruples p by A17, XBOOLE_0:def 5;

then [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in SepQuadruples p by A7;

hence [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y by A23, ZFMISC_1:56; :: thesis: verum

end;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,s)),t,K,f] in Y holds

[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

let x be Element of bound_QC-variables A; :: thesis: 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,s)),t,K,f] in Y holds

[s,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in Y

let u be QC-symbol of A; :: thesis: 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,s)),u,K,f] in Y holds

[s,(u ++),(K \/ {x}),(f +* (x .--> (x. u)))] in Y

let L be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,s)),u,L,f] in Y holds

[s,(u ++),(L \/ {x}),(f +* (x .--> (x. u)))] in Y

let h be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,s)),u,L,h] in Y implies [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y )

assume A17: [(All (x,s)),u,L,h] in Y ; :: thesis: [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y

now :: thesis: ( not [(All (x,q)),u,K,h] in SepQuadruples p & not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p & s = q implies not L \/ {x} = K )

then
( s <> q or u ++ <> t or L \/ {x} <> K or f <> h +* ({x} --> (x. u)) )
by A6;assume that

A18: not [(All (x,q)),u,K,h] in SepQuadruples p and

A19: not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ; :: thesis: ( s = q implies not L \/ {x} = K )

A20: ( s <> q or ( L <> K & L <> K \ {x} ) ) by A17, A18, A19, XBOOLE_0:def 5;

assume A21: s = q ; :: thesis: not L \/ {x} = K

assume A22: L \/ {x} = K ; :: thesis: contradiction

then K \ {x} = L \ {x} by XBOOLE_1:40;

hence contradiction by A20, A21, A22, ZFMISC_1:40, ZFMISC_1:57; :: thesis: verum

end;A18: not [(All (x,q)),u,K,h] in SepQuadruples p and

A19: not [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ; :: thesis: ( s = q implies not L \/ {x} = K )

A20: ( s <> q or ( L <> K & L <> K \ {x} ) ) by A17, A18, A19, XBOOLE_0:def 5;

assume A21: s = q ; :: thesis: not L \/ {x} = K

assume A22: L \/ {x} = K ; :: thesis: contradiction

then K \ {x} = L \ {x} by XBOOLE_1:40;

hence contradiction by A20, A21, A22, ZFMISC_1:40, ZFMISC_1:57; :: thesis: verum

then A23: [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] <> [q,t,K,f] by XTUPLE_0:5;

[(All (x,s)),u,L,h] in SepQuadruples p by A17, XBOOLE_0:def 5;

then [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in SepQuadruples p by A7;

hence [s,(u ++),(L \/ {x}),(h +* (x .--> (x. u)))] in Y by A23, ZFMISC_1:56; :: thesis: verum

then [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in Y by A2, ZFMISC_1:56;

then Y is_Sep-closed_on p by A8, A11, A16;

then SepQuadruples p c= Y by Def13;

then Y = SepQuadruples p by A15;

hence contradiction by A1, ZFMISC_1:57; :: thesis: verum