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