let x be set ; :: thesis: for G being addGroup
for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A * h = A ) )
let G be addGroup; :: thesis: for A being Subset of G holds
( x in Normalizer A iff ex h being Element of G st
( x = h & A * h = A ) )
let A be Subset of G; :: thesis: ( x in Normalizer A iff ex h being Element of G st
( x = h & A * h = A ) )
thus ( x in Normalizer A implies ex h being Element of G st
( x = h & A * h = A ) ) :: thesis: ( ex h being Element of G st
( x = h & A * h = A ) implies x in Normalizer A )

proof

assume x in Normalizer A ; :: thesis: ex h being Element of G st
( x = h & A * h = A )
then x in { h where h is Element of G : A * h = A } by Def14;
hence ex h being Element of G st
( x = h & A * h = A ) ; :: thesis: verum

end;

given h being Element of G such that A1: ( x = h & A * h = A ) ; :: thesis: x in Normalizer A
x in { b where b is Element of G : A * b = A } by A1;
hence x in Normalizer A by Def14; :: thesis: verum