let X be non empty set ; :: thesis: for A being non empty Subset of X holds
( A is trivial iff ex x being Element of X st A = {x} )
let A be non empty Subset of X; :: thesis: ( A is trivial iff ex x being Element of X st A = {x} )

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

assume A is trivial ; :: thesis: ex x being Element of X st A = {x}
then consider s being Element of A such that
A1: A = {s} by TEX_2:def 1;
thus ex x being Element of X st A = {x} by A1; :: thesis: verum

end;

given x being Element of X such that A2: A = {x} ; :: thesis: A is trivial
thus A is trivial by A2; :: thesis: verum