let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds p |- p
let p be Element of CQC-WFF A; :: thesis: p |- p
{p} |- p by CQC_THE2:87;
hence p |- p by Def1; :: thesis: verum