for G being Group
for a being Element of G
for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )