let X be set ; :: thesis: 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; :: thesis: ( X <> {} implies {x1,x2,x3} is Subset of X )
assume A1: X <> {} ; :: thesis: {x1,x2,x3} is Subset of X
then A2: x3 in X by Def2;
A3: ( x1 in X & x2 in X ) by A1, Def2;
{x1,x2,x3} c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3} or x in X )
assume x in {x1,x2,x3} ; :: thesis: x in X
hence x in X by A3, A2, ENUMSET1:def 1; :: thesis: verum

end;

then {x1,x2,x3} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3} is Subset of X by Def2; :: thesis: verum