VERUM in { s where s is QC-formula : ( Fixed s = {} & Free s = {} ) } by QC_LANG3:65, QC_LANG3:76;
hence not CQC-WFF is empty ; :: thesis: verum