let A be QC-alphabet ; :: thesis: for p, 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 holds
( [q,t,K,f] in SepQuadruples p & [r,(t + (QuantNbr q)),K,f] in SepQuadruples p )
let p be Element of CQC-WFF A; :: 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 holds
( [q,t,K,f] in SepQuadruples p & [r,(t + (QuantNbr q)),K,f] in SepQuadruples p )
SepQuadruples p is_Sep-closed_on p by Def13;
hence 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 holds
( [q,t,K,f] in SepQuadruples p & [r,(t + (QuantNbr q)),K,f] in SepQuadruples p ) ; :: thesis: verum