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