:: deftheorem Def13 defines SepQuadruples CQC_SIM1:def 13 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for b₃ being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds
( b₃ = SepQuadruples p iff ( b₃ is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds
b₃ c= D ) ) );