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 in {p} & {p} c= Cn {p} ) by CQC_THE1:17, TARSKI:def 1;
hence p in Cn {p} ; :: according to CQC_THE1:def 8 :: thesis: verum