theorem Th67: :: GROUP_4:67

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