let p be Element of CQC-WFF ; :: thesis: p => (p '&' p) in TAUT
( ('not' (p '&' p)) => (('not' p) 'or' ('not' p)) in TAUT & (('not' p) 'or' ('not' p)) => ('not' p) in TAUT ) by Th11, Th17;
then ('not' (p '&' p)) => ('not' p) in TAUT by LUKASI_1:3;
hence p => (p '&' p) in TAUT by LUKASI_1:35; :: thesis: verum