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