let p, q be Element of CQC-WFF ; :: thesis: (p '&' q) => q in TAUT
( (q '&' p) => q in TAUT & (p '&' q) => (q '&' p) in TAUT ) by Th19, CQC_THE1:81;
hence (p '&' q) => q in TAUT by LUKASI_1:3; :: thesis: verum