let X, x be set ; :: thesis: ( X,{x} are_equipotent iff ex x being set st X = {x} )
thus ( X,{x} are_equipotent implies ex x being set st X = {x} ) :: thesis: ( ex x being set st X = {x} implies X,{x} are_equipotent )

proof

assume X,{x} are_equipotent ; :: thesis: ex x being set st X = {x}
then consider f being Function such that
A1: ( f is one-to-one & dom f = {x} & rng f = X ) by WELLORD2:def 4;
rng f = {(f . x)} by A1, FUNCT_1:14;
hence ex x being set st X = {x} by A1; :: thesis: verum

end;

given y being set such that A2: X = {y} ; :: thesis: X,{x} are_equipotent
take f = X --> x; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = {x} )
A3: ( dom f = X & ( for y being set st y in X holds
f . y = x ) ) by FUNCOP_1:13, FUNCOP_1:19;
thus f is one-to-one :: thesis: ( dom f = X & rng f = {x} )

proof

let a be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not a in dom f or not b₁ in dom f or not f . a = f . b₁ or a = b₁ )
let b be set ; :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume ( a in dom f & b in dom f & f . a = f . b ) ; :: thesis: a = b
then ( a = y & b = y ) by A2, A3, TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

thus dom f = X by FUNCOP_1:19; :: thesis: rng f = {x}
thus rng f c= {x} by FUNCOP_1:19; :: according to XBOOLE_0:def 10 :: thesis: {x} c= rng f
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} or a in rng f )
assume a in {x} ; :: thesis: a in rng f
then A4: ( a = x & y in {y} ) by TARSKI:def 1;
then f . y = x by A2, FUNCOP_1:13;
hence a in rng f by A2, A3, A4, FUNCT_1:def 5; :: thesis: verum