let X be set ; 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; ( 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 <> {}
; {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 ;
TARSKI:def 3 ( 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;
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; verum