let X be set ; :: thesis: for x1 being Element of X st X <> {} holds
{x1} is Subset of X
let x1 be Element of X; :: thesis: ( X <> {} implies {x1} is Subset of X )
assume X <> {} ; :: thesis: {x1} is Subset of X
then A1: x1 in X by Def1;
{x1} c= X by A1, TARSKI:def 1;
then {x1} in bool X by ZFMISC_1:def 1;
hence {x1} is Subset of X by Def1; :: thesis: verum