hereby :: thesis: ( ex s being Element of X st X = {s} implies X is trivial )

assume X is trivial ; :: thesis: ex s being Element of X st X = {s}
then consider s being set such that
A1: X = {s} by REALSET1:def 4;
s in X by A1, TARSKI:def 1;
hence ex s being Element of X st X = {s} by A1; :: thesis: verum

end;

thus ( ex s being Element of X st X = {s} implies X is trivial ) ; :: thesis: verum