let p be Element of CQC-WFF ; :: thesis: ( p => VERUM is valid & ('not' VERUM) => p is valid )
thus p => VERUM in TAUT by Th13, CQC_THE1:41; :: according to CQC_THE1:def 10 :: thesis: ('not' VERUM) => p is valid
thus ('not' VERUM) => p in TAUT by Th12; :: according to CQC_THE1:def 10 :: thesis: verum