let X be Subset of CQC-WFF ; :: thesis: X |- VERUM
VERUM in Cn X by Th27;
hence X |- VERUM by Def9; :: thesis: verum