for G being Group
for H1, H2 being Subgroup of G holds
( H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2 )