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