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