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

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

end;

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

now :: thesis: for a, b being Element of G holds a = b

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 ; :: thesis: verum