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