let X be set ; :: thesis: for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
let x1, x2, x3, x4, x5, x6, x7 be Element of X; :: thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X )
set A = {x1,x2,x3,x4,x5,x6,x7};
assume A1: X <> {} ; :: thesis: {x1,x2,x3,x4,x5,x6,x7} is Subset of X
{x1,x2,x3,x4,x5,x6,x7} c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x in X )
( not x in {x1,x2,x3,x4,x5,x6,x7} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) by ENUMSET1:def 5;
hence ( not x in {x1,x2,x3,x4,x5,x6,x7} or x in X ) by A1, Def1; :: thesis: verum

end;

then {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def 1;
hence {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def1; :: thesis: verum