let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in HP_TAUT implies q '&' p in HP_TAUT )
assume A1: p '&' q in HP_TAUT ; :: thesis: q '&' p in HP_TAUT
then A2: q in HP_TAUT by Th31;
p in HP_TAUT by A1, Th31;
hence q '&' p in HP_TAUT by A2, Th31; :: thesis: verum