let p be Element of CQC-WFF ; :: thesis: ('not' VERUM ) => p in TAUT
VERUM => (('not' VERUM ) => p) in TAUT by CQC_THE1:79;
hence ('not' VERUM ) => p in TAUT by CQC_THE1:77, CQC_THE1:82; :: thesis: verum