let p be Element of CQC-WFF ; :: thesis: 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 SepQuadruples p holds
( [q,k,K,f] in SepQuadruples p & [r,(k + (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
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 holds
( [q,k,K,f] in SepQuadruples p & [r,(k + (QuantNbr q)),K,f] in SepQuadruples p ) by Def12; :: thesis: verum