let A be QC-alphabet ; :: thesis: for p, 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 [q,t,K,f] in SepQuadruples p holds
q is_subformula_of p
let p be Element of CQC-WFF A; :: thesis: 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 [q,t,K,f] in SepQuadruples p holds
q is_subformula_of p
defpred S₁[ Element of CQC-WFF A, set , set , set ] means $1 is_subformula_of p;

A1: now :: thesis: 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 SepQuadruples p & S₁[ 'not' q,t,K,f] holds
S₁[q,t,K,f]

let q 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' q),t,K,f] in SepQuadruples p & S₁[ 'not' q,t,K,f] holds
S₁[q,t,K,f]
let t 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' q),t,K,f] in SepQuadruples p & S₁[ 'not' q,t,K,f] holds
S₁[q,t,K,f]
let K 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' q),t,K,f] in SepQuadruples p & S₁[ 'not' q,t,K,f] holds
S₁[q,t,K,f]
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [('not' q),t,K,f] in SepQuadruples p & S₁[ 'not' q,t,K,f] implies S₁[q,t,K,f] )
assume [('not' q),t,K,f] in SepQuadruples p ; :: thesis: ( S₁[ 'not' q,t,K,f] implies S₁[q,t,K,f] )
q is_subformula_of 'not' q by Th10;
hence ( S₁[ 'not' q,t,K,f] implies S₁[q,t,K,f] ) by QC_LANG2:57; :: thesis: verum

end;

A2: now :: thesis: 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 SepQuadruples p & S₁[ All (x,q),t,K,f] holds
S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

let q 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,q)),t,K,f] in SepQuadruples p & S₁[ All (x,q),t,K,f] holds
S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
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,q)),t,K,f] in SepQuadruples p & S₁[ All (x,q),t,K,f] holds
S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
let t 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,q)),t,K,f] in SepQuadruples p & S₁[ All (x,q),t,K,f] holds
S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
let K 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,q)),t,K,f] in SepQuadruples p & S₁[ All (x,q),t,K,f] holds
S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(All (x,q)),t,K,f] in SepQuadruples p & S₁[ All (x,q),t,K,f] implies S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )
assume [(All (x,q)),t,K,f] in SepQuadruples p ; :: thesis: ( S₁[ All (x,q),t,K,f] implies S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] )
q is_subformula_of All (x,q) by Th12;
hence ( S₁[ All (x,q),t,K,f] implies S₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] ) by QC_LANG2:57; :: thesis: verum

end;

A3: now :: thesis: 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 SepQuadruples p & S₁[q '&' r,t,K,f] holds
( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] )

let q, 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 [(q '&' r),t,K,f] in SepQuadruples p & S₁[q '&' r,t,K,f] holds
( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] )
let t 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 [(q '&' r),t,K,f] in SepQuadruples p & S₁[q '&' r,t,K,f] holds
( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] )
let K be Element of Fin (bound_QC-variables A); :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p & S₁[q '&' r,t,K,f] holds
( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] )
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: ( [(q '&' r),t,K,f] in SepQuadruples p & S₁[q '&' r,t,K,f] implies ( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] ) )
assume [(q '&' r),t,K,f] in SepQuadruples p ; :: thesis: ( S₁[q '&' r,t,K,f] implies ( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] ) )
A4: r is_subformula_of q '&' r by Th11;
q is_subformula_of q '&' r by Th11;
hence ( S₁[q '&' r,t,K,f] implies ( S₁[q,t,K,f] & S₁[r,t + (QuantNbr q),K,f] ) ) by A4, QC_LANG2:57; :: thesis: verum

end;

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