hereby :: thesis: ( ex x being set st the carrier of G = {x} implies G is trivial )

set y = the Element of G;
assume G is trivial ; :: thesis: ex x being set st the carrier of G = {x}
then for x being set holds
( x in the carrier of G iff x = the Element of G ) by STRUCT_0:def 10;
then the carrier of G = { the Element of G} by TARSKI:def 1;
hence ex x being set st the carrier of G = {x} ; :: thesis: verum

end;

given x being set such that A1: the carrier of G = {x} ; :: thesis: G is trivial

now

let a, b be Element of G; :: thesis: a = b
thus a = x by A1, TARSKI:def 1
.= b by A1, TARSKI:def 1 ; :: thesis: verum

end;

hence G is trivial by STRUCT_0:def 10; :: thesis: verum