theorem Th37: :: GROUP_4:37

for G being strict Group
for H being strict Subgroup of G
for a being Element of G st H is maximal & not a in H holds
gr ((carr H) \/ {a}) = G