let p, q be Element of HP-WFF ; :: thesis: ( p '&' q in HP_TAUT iff q '&' p in HP_TAUT )

hereby :: thesis: ( q '&' p in HP_TAUT implies p '&' q in HP_TAUT )

assume p '&' q in HP_TAUT ; :: thesis: q '&' p in HP_TAUT
then ( p in HP_TAUT & q in HP_TAUT ) by Th31;
hence q '&' p in HP_TAUT by Th31; :: thesis: verum

end;

assume q '&' p in HP_TAUT ; :: thesis: p '&' q in HP_TAUT
then ( q in HP_TAUT & p in HP_TAUT ) by Th31;
hence p '&' q in HP_TAUT by Th31; :: thesis: verum