let A be QC-alphabet ; :: thesis: VERUM A is Element of CQC-WFF A
( Fixed (VERUM A) = {} & Free (VERUM A) = {} ) by QC_LANG3:53, QC_LANG3:63;
hence VERUM A is Element of CQC-WFF A by Th4; :: thesis: verum