let p be Element of CQC-WFF ; :: thesis: p |- p
{p} |- p by CQC_THE2:87;
hence p |- p by Def1; :: thesis: verum