for G being Group
for H1, H2 being strict Subgroup of G holds
( H1 "\/" H2 = H2 iff H1 /\ H2 = H1 )