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