theorem Th18: :: GROUP_23:23

for G, H being Group
for h being Element of H st H is Subgroup of G holds
(incl (H,G)) . h = h