let X be non empty set ; :: thesis: for f being Subset of X st f is Element of singletons X holds

f is 1 -element

let f be Subset of X; :: thesis: ( f is Element of singletons X implies f is 1 -element )

assume f is Element of singletons X ; :: thesis: f is 1 -element

then f in singletons X ;

then ex g being Subset of X st

( g = f & g is 1 -element ) ;

hence f is 1 -element ; :: thesis: verum

f is 1 -element

let f be Subset of X; :: thesis: ( f is Element of singletons X implies f is 1 -element )

assume f is Element of singletons X ; :: thesis: f is 1 -element

then f in singletons X ;

then ex g being Subset of X st

( g = f & g is 1 -element ) ;

hence f is 1 -element ; :: thesis: verum