let G be Group; :: thesis: for g, h being Element of G st ( h * g = h or g * h = h ) holds
g = 1_ G
let g, h be Element of G; :: thesis: ( ( h * g = h or g * h = h ) implies g = 1_ G )
( h * (1_ G) = h & (1_ G) * h = h ) by Def4;
hence ( ( h * g = h or g * h = h ) implies g = 1_ G ) by Th6; :: thesis: verum