let p be Element of CQC-WFF ; :: thesis: 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 [q,k,K,f] in SepQuadruples p holds
still_not-bound_in q c= (still_not-bound_in p) \/ K
deffunc H₆( QC-formula) -> Element of bool bound_QC-variables = still_not-bound_in $1;
defpred S₁[ QC-formula, set , set , set ] means H₆($1) c= H₆(p) \/ $3;
A1: 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 SepQuadruples p & S₁[ 'not' q,k,K,f] holds
S₁[q,k,K,f] by QC_LANG3:7;

A2: now

let q, r be Element of CQC-WFF ; :: thesis: 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 SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let k be Element of NAT ; :: thesis: 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 SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let K be Finite_Subset of bound_QC-variables; :: thesis: for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] holds
( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: ( [(q '&' r),k,K,f] in SepQuadruples p & S₁[q '&' r,k,K,f] implies ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] ) )
assume that
[(q '&' r),k,K,f] in SepQuadruples p and
A3: S₁[q '&' r,k,K,f] ; :: thesis: ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] )
A4: still_not-bound_in (q '&' r) = (still_not-bound_in q) \/ (still_not-bound_in r) by QC_LANG3:10;
then A5: still_not-bound_in r c= still_not-bound_in (q '&' r) by XBOOLE_1:7;
still_not-bound_in q c= still_not-bound_in (q '&' r) by A4, XBOOLE_1:7;
hence ( S₁[q,k,K,f] & S₁[r,k + (QuantNbr q),K,f] ) by A3, A5, XBOOLE_1:1; :: thesis: verum

end;

A6: now

let q be Element of CQC-WFF ; :: thesis: 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 SepQuadruples p & S₁[ All (x,q),k,K,f] holds
S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))]
let x be Element of bound_QC-variables ; :: thesis: 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 SepQuadruples p & S₁[ All (x,q),k,K,f] holds
S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))]
let k be Element of NAT ; :: thesis: 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 SepQuadruples p & S₁[ All (x,q),k,K,f] holds
S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))]
let K be Finite_Subset of bound_QC-variables; :: thesis: for f being Element of Funcs (bound_QC-variables,bound_QC-variables) st [(All (x,q)),k,K,f] in SepQuadruples p & S₁[ All (x,q),k,K,f] holds
S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))]
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: ( [(All (x,q)),k,K,f] in SepQuadruples p & S₁[ All (x,q),k,K,f] implies S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))] )
assume that
[(All (x,q)),k,K,f] in SepQuadruples p and
A7: S₁[ All (x,q),k,K,f] ; :: thesis: S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))]
still_not-bound_in (All (x,q)) = (still_not-bound_in q) \ {x} by QC_LANG3:12;
then still_not-bound_in q c= ((still_not-bound_in p) \/ K) \/ {x} by A7, XBOOLE_1:44;
hence S₁[q,k + 1,K \/ {x},f +* (x .--> (x. k))] by XBOOLE_1:4; :: thesis: verum

end;

A8: S₁[p, index p, {}. bound_QC-variables, id bound_QC-variables] ;
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 [q,k,K,f] in SepQuadruples p holds
S₁[q,k,K,f] from CQC_SIM1:sch 6(A8, A1, A2, A6); :: thesis: verum