let x be set ; :: thesis: for G being Group
for A being Subset of G holds
( x in Normalizator 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 Normalizator A iff ex h being Element of G st
( x = h & A |^ h = A ) )
let A be Subset of G; :: thesis: ( x in Normalizator A iff ex h being Element of G st
( x = h & A |^ h = A ) )
thus ( x in Normalizator 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 Normalizator A )

proof

assume x in Normalizator A ; :: thesis: ex h being Element of G st
( x = h & A |^ h = A )
then x in the carrier of (Normalizator 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 Normalizator A
x in { b where b is Element of G : A |^ b = A } by A1;
then x in the carrier of (Normalizator A) by Def14;
hence x in Normalizator A by STRUCT_0:def 5; :: thesis: verum