let p be Element of CQC-WFF ; :: thesis: {p} |- p
( p in {p} & {p} c= Cn {p} ) by CQC_THE1:38, TARSKI:def 1;
hence p in Cn {p} ; :: according to CQC_THE1:def 9 :: thesis: verum