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)
( (H2 "\/" H3) "\/" H1 is Subgroup of H2 "\/" (H3 "\/" H1) & (H3 "\/" H1) "\/" H2 is Subgroup of H3 "\/" (H1 "\/" H2) ) by Lm5;
then A1: H1 "\/" (H2 "\/" H3) is Subgroup of H3 "\/" (H1 "\/" H2) by GROUP_2:56;
(H1 "\/" H2) "\/" H3 is Subgroup of H1 "\/" (H2 "\/" H3) by Lm5;
hence (H1 "\/" H2) "\/" H3 = H1 "\/" (H2 "\/" H3) by A1, GROUP_2:55; :: thesis: verum