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