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;
consider d being Element of Y;
reconsider D = {d} as Subset of Y ;
take d ; :: thesis: the carrier of Y = {d}

now

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

end;

then A c= D by SUBSET_1:7;
hence the carrier of Y = {d} 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

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 by STRUCT_0:def 10; :: thesis: verum