let G be Group; :: thesis: for H1, H2, H3 being Subgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
let H1, H2, H3 be Subgroup of G; :: thesis: (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)
the carrier of ((H1 /\ H2) /\ H3) = (carr (H1 /\ H2)) /\ (carr H3) by Def10
.= ((carr H1) /\ (carr H2)) /\ (carr H3) by Def10
.= (carr H1) /\ ((carr H2) /\ (carr H3)) by XBOOLE_1:16
.= (carr H1) /\ (carr (H2 /\ H3)) by Def10
.= the carrier of (H1 /\ (H2 /\ H3)) by Def10 ;
hence (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3) by Th59; :: thesis: verum