let x be set ; :: thesis: for G being Group
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 Group; :: 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 the carrier of (Normalizer A) by STRUCT_0:def 5;
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;
then x in the carrier of (Normalizer A) by Def14;
hence x in Normalizer A by STRUCT_0:def 5; :: thesis: verum