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 [('not' q),k,K,f] in SepQuadruples p holds
[q,k,K,f] in SepQuadruples p
SepQuadruples p is_Sep-closed_on p by Def13;
hence 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 holds
[q,k,K,f] in SepQuadruples p by Def12; :: thesis: verum