let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds 'not' (p '&' ('not' p)) in TAUT A
let p be Element of CQC-WFF A; :: thesis: 'not' (p '&' ('not' p)) in TAUT A
p => p in TAUT A by LUKASI_1:4;
hence 'not' (p '&' ('not' p)) in TAUT A by QC_LANG2:def 2; :: thesis: verum