let X be non empty set ; :: thesis: ( ex s being object st
for r being object st r in X holds
s = r implies ex r being object st X = {r} )
assume ex s being object st
for r being object st r in X holds
s = r ; :: thesis: ex r being object st X = {r}
then consider s0 being object such that
A1: for r being object st r in X holds
s0 = r ;
set r0 = the Element of X;
take the Element of X ; :: thesis: X = { the Element of X}
thus X c= { the Element of X} :: according to XBOOLE_0:def 10 :: thesis: { the Element of X} c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { the Element of X} )
assume A3: x in X ; :: thesis: x in { the Element of X}
the Element of X = s0 by A1
.= x by A1, A3 ;
hence x in { the Element of X} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Element of X} or x in X )
assume x in { the Element of X} ; :: thesis: x in X
then x = the Element of X by TARSKI:def 1;
hence x in X ; :: thesis: verum