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