let X be set ; :: thesis: for s being Subset of X st s is 1 -element holds
ex x being set st
( x in X & s = {x} )
let s be Subset of X; :: thesis: ( s is 1 -element implies ex x being set st
( x in X & s = {x} ) )
assume s is 1 -element ; :: thesis: ex x being set st
( x in X & s = {x} )
then ( s is trivial & not s is empty ) ;
then consider x being Element of s such that
A1: s = {x} by SUBSET_1:46;
take x ; :: thesis: ( x in X & s = {x} )
x in s by A1;
hence x in X ; :: thesis: s = {x}
thus s = {x} by A1; :: thesis: verum