theorem Th58: :: GROUP_3:58

for x being set
for G being Group
for a being Element of G
for H being Subgroup of G holds
( x in H |^ a iff ex g being Element of G st
( x = g |^ a & g in H ) )