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