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 )

( 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

thus
( x = 1_ G implies x in (1). G )
by GROUP_2:46; :: thesis: verum
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;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