let p, q, s be Element of HP-WFF ; :: thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
set P = (p '&' q) '&' s;
set Q = p '&' s;
A1: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by Lm8;
(((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT by Th41;
hence (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by A1, Def10; :: thesis: verum