let x be set ; :: thesis: for G being Group holds
( x in (1). G iff x = 1_ G )
let G be Group; :: thesis: ( x in (1). G iff x = 1_ G )
thus ( x in (1). G implies x = 1_ G ) :: thesis: ( x = 1_ G implies x in (1). G )

proof

assume x in (1). G ; :: thesis: x = 1_ G
then x in the carrier of ((1). G) by STRUCT_0:def 5;
then x in {(1_ G)} by GROUP_2:def 7;
hence x = 1_ G by TARSKI:def 1; :: thesis: verum

end;

thus ( x = 1_ G implies x in (1). G ) by GROUP_2:46; :: thesis: verum