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:77; :: according to CQC_THE1:def 11 :: thesis: ('not' VERUM ) => p is valid
thus ('not' VERUM ) => p in TAUT by Th12; :: according to CQC_THE1:def 11 :: thesis: verum