thus ( f is Singleton implies ex x being set st
( x in X & f = {x} ) ) :: thesis: ( ex x being set st
( x in X & f = {x} ) implies f is Singleton )

proof

assume f is Singleton ; :: thesis: ex x being set st
( x in X & f = {x} )
then consider x being set such that
A1: f = {x} by REALSET1:def 4;
take x ; :: thesis: ( x in X & f = {x} )
x in f by A1, TARSKI:def 1;
hence x in X ; :: thesis: f = {x}
thus f = {x} by A1; :: thesis: verum

end;

thus ( ex x being set st
( x in X & f = {x} ) implies f is Singleton ) ; :: thesis: verum