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