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