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