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