hereby :: thesis: ( ex d being Element of Y st the carrier of Y = {d} implies Y is trivial )

assume A1: Y is trivial ; :: thesis: ex d being Element of Y st the carrier of Y = {d}
thus ex d being Element of Y st the carrier of Y = {d} :: thesis: verum

proof

reconsider A = the carrier of Y as Subset of Y by Lm1;
set d = the Element of Y;
reconsider D = { the Element of Y} as Subset of Y ;
take the Element of Y ; :: thesis: the carrier of Y = { the Element of Y}

now :: thesis: for a being Element of Y st a in A holds
a in D

let a be Element of Y; :: thesis: ( a in A implies a in D )
assume a in A ; :: thesis: a in D
a = the Element of Y by A1;
hence a in D by TARSKI:def 1; :: thesis: verum

end;

then A c= D by SUBSET_1:2;
hence the carrier of Y = { the Element of Y} by XBOOLE_0:def 10; :: thesis: verum

end;

end;

given d being Element of Y such that A2: the carrier of Y = {d} ; :: thesis: Y is trivial

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

let a, b be Element of Y; :: thesis: a = b
a = d by A2, TARSKI:def 1;
hence a = b by A2, TARSKI:def 1; :: thesis: verum

end;

hence Y is trivial ; :: thesis: verum