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