let H1, H2 be Subgroup of G; :: thesis: H1 /\ H2 = H2 /\ H1
the carrier of (H1 /\ H2) = (carr H2) /\ (carr H1) by Def10
.= the carrier of (H2 /\ H1) by Def10 ;
hence H1 /\ H2 = H2 /\ H1 by Th59; :: thesis: verum