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