let X be non empty set ; :: thesis: for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
let A be non empty Subset of X; :: thesis: ( A is trivial implies ex x being Element of X st A = {x} )
assume A is trivial ; :: thesis: ex x being Element of X st A = {x}
then ex s being Element of A st A = {s} by Th46;
hence ex x being Element of X st A = {x} ; :: thesis: verum