let X, x be set ; :: thesis: ( x in X implies {x} is Subset of X )
assume x in X ; :: thesis: {x} is Subset of X
then {x} c= X by ZFMISC_1:31;
then {x} in bool X by ZFMISC_1:def 1;
hence {x} is Subset of X by Def1; :: thesis: verum