theorem :: GROUP_4:56
for G being Group
for H1, H2 being Subgroup of G holds H1 "\/" H2 = H2 "\/" H1 ;