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