let p be Element of CQC-WFF ; :: thesis: [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples p
SepQuadruples p is_Sep-closed_on p by Def13;
hence [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples p by Def12; :: thesis: verum