let G be Group; :: thesis: ( G is trivial iff for x being Element of G holds x = 1_ G )
thus ( G is trivial implies for x being Element of G holds x = 1_ G ) ; :: thesis: ( ( for x being Element of G holds x = 1_ G ) implies G is trivial )
assume A2: for x being Element of G holds x = 1_ G ; :: thesis: G is trivial
for x being object holds
( x in the carrier of G iff x in {(1_ G)} )

proof

let x be object ; :: thesis: ( x in the carrier of G iff x in {(1_ G)} )

hereby :: thesis: ( x in {(1_ G)} implies x in the carrier of G )

assume x in the carrier of G ; :: thesis: x in {(1_ G)}
then x = 1_ G by A2;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

assume x in {(1_ G)} ; :: thesis: x in the carrier of G
hence x in the carrier of G ; :: thesis: verum

end;

hence G is trivial by TARSKI:2; :: thesis: verum