:: ENUMSET1 semantic presentation

begin

              Lm1:  for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
proof
let x, X, y be set ; ::_thesis: ( x in union {X,{y}} iff ( x in X or x = y ) )
A1: ( not x in union {X,{y}} or x in X or x in {y} )
proof
assume  x in union {X,{y}} ; ::_thesis: ( x in X or x in {y} )
then  ex Z being set st
( x in Z & Z in {X,{y}} ) by TARSKI:def_4;
hence  ( x in X or x in {y} ) by TARSKI:def_2; ::_thesis: verum
end;
A2: ( x in {y} iff x = y ) by TARSKI:def_1;
 ( X in {X,{y}} & {y} in {X,{y}} ) by TARSKI:def_2;
hence  ( x in union {X,{y}} iff ( x in X or x = y ) ) by A1, A2, TARSKI:def_4; ::_thesis: verum
end;

definition
let x1, x2, x3 be set ;
func{x1,x2,x3} ->  set  means :Def1: :: ENUMSET1:def 1
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) )
proof
take  union {{x1,x2},{x3}} ; ::_thesis: for x being set holds
( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) )
 ( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def_2;
hence  ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines { ENUMSET1:def_1_:_
 for x1, x2, x3, b4 being set holds
( b4 = {x1,x2,x3} iff for x being set holds
( x in b4 iff ( x = x1 or x = x2 or x = x3 ) ) );

definition
let x1, x2, x3, x4 be set ;
func{x1,x2,x3,x4} ->  set  means :Def2: :: ENUMSET1:def 2
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
proof
take  union {{x1,x2,x3},{x4}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
 ( x in {x1,x2,x3} iff ( x = x1 or x = x2 or x = x3 ) ) by Def1;
hence  ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines { ENUMSET1:def_2_:_
 for x1, x2, x3, x4, b5 being set holds
( b5 = {x1,x2,x3,x4} iff for x being set holds
( x in b5 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) );

definition
let x1, x2, x3, x4, x5 be set ;
func{x1,x2,x3,x4,x5} ->  set  means :Def3: :: ENUMSET1:def 3
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
proof
take  union {{x1,x2,x3,x4},{x5}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
 ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2;
hence  ( x in union {{x1,x2,x3,x4},{x5}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines { ENUMSET1:def_3_:_
 for x1, x2, x3, x4, x5, b6 being set holds
( b6 = {x1,x2,x3,x4,x5} iff for x being set holds
( x in b6 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) );

definition
let x1, x2, x3, x4, x5, x6 be set ;
func{x1,x2,x3,x4,x5,x6} ->  set  means :Def4: :: ENUMSET1:def 4
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
proof
take  union {{x1,x2,x3,x4,x5},{x6}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
 ( x in {x1,x2,x3,x4,x5} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Def3;
hence  ( x in union {{x1,x2,x3,x4,x5},{x6}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines { ENUMSET1:def_4_:_
 for x1, x2, x3, x4, x5, x6, b7 being set holds
( b7 = {x1,x2,x3,x4,x5,x6} iff for x being set holds
( x in b7 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) );

definition
let x1, x2, x3, x4, x5, x6, x7 be set ;
func{x1,x2,x3,x4,x5,x6,x7} ->  set  means :Def5: :: ENUMSET1:def 5
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )
proof
take  union {{x1,x2,x3,x4,x5,x6},{x7}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )
 ( x in {x1,x2,x3,x4,x5,x6} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Def4;
hence  ( x in union {{x1,x2,x3,x4,x5,x6},{x7}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 or $1 = x7 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines { ENUMSET1:def_5_:_
 for x1, x2, x3, x4, x5, x6, x7, b8 being set holds
( b8 = {x1,x2,x3,x4,x5,x6,x7} iff for x being set holds
( x in b8 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) );

definition
let x1, x2, x3, x4, x5, x6, x7, x8 be set ;
func{x1,x2,x3,x4,x5,x6,x7,x8} ->  set  means :Def6: :: ENUMSET1:def 6
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )
proof
take  union {{x1,x2,x3,x4,x5,x6,x7},{x8}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )
 ( x in {x1,x2,x3,x4,x5,x6,x7} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) by Def5;
hence  ( x in union {{x1,x2,x3,x4,x5,x6,x7},{x8}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 or $1 = x7 or $1 = x8 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines { ENUMSET1:def_6_:_
 for x1, x2, x3, x4, x5, x6, x7, x8, b9 being set holds
( b9 = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being set holds
( x in b9 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) );

definition
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ;
func{x1,x2,x3,x4,x5,x6,x7,x8,x9} ->  set  means :Def7: :: ENUMSET1:def 7
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) )
proof
take  union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) )
 ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) by Def6;
hence  ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8},{x9}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 or $1 = x7 or $1 = x8 or $1 = x9 );
thus  for X, Y being set st ( for x being set holds
( x in X iff S1[x] ) ) & ( for x being set holds
( x in Y iff S1[x] ) ) holds
X = Y from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def7 defines { ENUMSET1:def_7_:_
 for x1, x2, x3, x4, x5, x6, x7, x8, x9, b10 being set holds
( b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds
( x in b10 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) );

definition
let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ;
func{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ->  set  means :Def8: :: ENUMSET1:def 8
 for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )
proof
take  union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} ; ::_thesis: for x being set holds
( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )
let x be set ; ::_thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )
 ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Def7;
hence  ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ( $1 = x1 or $1 = x2 or $1 = x3 or $1 = x4 or $1 = x5 or $1 = x6 or $1 = x7 or $1 = x8 or $1 = x9 or $1 = x10 );
thus  for X, Y being set st ( for x being set holds
( x in X iff S1[x] ) ) & ( for x being set holds
( x in Y iff S1[x] ) ) holds
X = Y from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def8 defines { ENUMSET1:def_8_:_
 for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b11 being set holds
( b11 = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being set holds
( x in b11 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) );

theorem Th1: :: ENUMSET1:1
for x1, x2 being set holds {x1,x2} = {x1} \/ {x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x2} = {x1} \/ {x2}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2}_iff_x_in_{x1}_\/_{x2}_)
let x be set ; ::_thesis: ( x in {x1,x2} iff x in {x1} \/ {x2} )
 ( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def_2;
then  ( x in {x1,x2} iff ( x in {x1} or x in {x2} ) ) by TARSKI:def_1;
hence  ( x in {x1,x2} iff x in {x1} \/ {x2} ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2} = {x1} \/ {x2} by TARSKI:1; ::_thesis: verum
end;

theorem Th2: :: ENUMSET1:2
for x1, x2, x3 being set holds {x1,x2,x3} = {x1} \/ {x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1} \/ {x2,x3}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3}_iff_x_in_{x1}_\/_{x2,x3}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3} iff x in {x1} \/ {x2,x3} )
 ( x in {x1,x2,x3} iff ( x = x1 or x = x2 or x = x3 ) ) by Def1;
then  ( x in {x1,x2,x3} iff ( x in {x1} or x in {x2,x3} ) ) by TARSKI:def_1, TARSKI:def_2;
hence  ( x in {x1,x2,x3} iff x in {x1} \/ {x2,x3} ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3} = {x1} \/ {x2,x3} by TARSKI:1; ::_thesis: verum
end;

theorem Th3: :: ENUMSET1:3
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x2} \/ {x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1,x2} \/ {x3}
thus {x1,x2,x3} = {x1} \/ {x2,x3} by Th2
.= {x1} \/ ({x2} \/ {x3}) by Th1
.= ({x1} \/ {x2}) \/ {x3} by XBOOLE_1:4
.= {x1,x2} \/ {x3} by Th1 ; ::_thesis: verum
end;

Lm2:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4}_iff_x_in_{x1,x2}_\/_{x3,x4}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4} iff x in {x1,x2} \/ {x3,x4} )
 ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2;
then  ( x in {x1,x2,x3,x4} iff ( x in {x1,x2} or x in {x3,x4} ) ) by TARSKI:def_2;
hence  ( x in {x1,x2,x3,x4} iff x in {x1,x2} \/ {x3,x4} ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by TARSKI:1; ::_thesis: verum
end;

theorem Th4: :: ENUMSET1:4
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
thus {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2
.= ({x1} \/ {x2}) \/ {x3,x4} by Th1
.= {x1} \/ ({x2} \/ {x3,x4}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4} by Th2 ; ::_thesis: verum
end;

theorem :: ENUMSET1:5
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2;

theorem Th6: :: ENUMSET1:6
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
thus {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2
.= {x1,x2} \/ ({x3} \/ {x4}) by Th1
.= ({x1,x2} \/ {x3}) \/ {x4} by XBOOLE_1:4
.= {x1,x2,x3} \/ {x4} by Th3 ; ::_thesis: verum
end;

Lm3:  for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5}_iff_x_in_{x1,x2,x3}_\/_{x4,x5}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} )
 ( x in {x1,x2,x3,x4,x5} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) by Def3;
then  ( x in {x1,x2,x3,x4,x5} iff ( x in {x1,x2,x3} or x in {x4,x5} ) ) by Def1, TARSKI:def_2;
hence  ( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by TARSKI:1; ::_thesis: verum
end;

theorem Th7: :: ENUMSET1:7
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3
.= ({x1} \/ {x2,x3}) \/ {x4,x5} by Th2
.= {x1} \/ ({x2,x3} \/ {x4,x5}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4,x5} by Lm2 ; ::_thesis: verum
end;

theorem Th8: :: ENUMSET1:8
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3
.= ({x1,x2} \/ {x3}) \/ {x4,x5} by Th3
.= {x1,x2} \/ ({x3} \/ {x4,x5}) by XBOOLE_1:4
.= {x1,x2} \/ {x3,x4,x5} by Th2 ; ::_thesis: verum
end;

theorem :: ENUMSET1:9
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3;

theorem Th10: :: ENUMSET1:10
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
thus {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3
.= {x1,x2,x3} \/ ({x4} \/ {x5}) by Th1
.= ({x1,x2,x3} \/ {x4}) \/ {x5} by XBOOLE_1:4
.= {x1,x2,x3,x4} \/ {x5} by Th6 ; ::_thesis: verum
end;

Lm4:  for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5,x6}_iff_x_in_{x1,x2,x3}_\/_{x4,x5,x6}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6} iff x in {x1,x2,x3} \/ {x4,x5,x6} )
 ( x in {x1,x2,x3,x4,x5,x6} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) by Def4;
then  ( x in {x1,x2,x3,x4,x5,x6} iff ( x in {x1,x2,x3} or x in {x4,x5,x6} ) ) by Def1;
hence  ( x in {x1,x2,x3,x4,x5,x6} iff x in {x1,x2,x3} \/ {x4,x5,x6} ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by TARSKI:1; ::_thesis: verum
end;

theorem Th11: :: ENUMSET1:11
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}
thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4
.= ({x1} \/ {x2,x3}) \/ {x4,x5,x6} by Th2
.= {x1} \/ ({x2,x3} \/ {x4,x5,x6}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4,x5,x6} by Th8 ; ::_thesis: verum
end;

theorem Th12: :: ENUMSET1:12
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}
thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4
.= ({x1,x2} \/ {x3}) \/ {x4,x5,x6} by Th3
.= {x1,x2} \/ ({x3} \/ {x4,x5,x6}) by XBOOLE_1:4
.= {x1,x2} \/ {x3,x4,x5,x6} by Th4 ; ::_thesis: verum
end;

theorem :: ENUMSET1:13
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4;

theorem Th14: :: ENUMSET1:14
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}
thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4
.= {x1,x2,x3} \/ ({x4} \/ {x5,x6}) by Th2
.= ({x1,x2,x3} \/ {x4}) \/ {x5,x6} by XBOOLE_1:4
.= {x1,x2,x3,x4} \/ {x5,x6} by Th6 ; ::_thesis: verum
end;

theorem :: ENUMSET1:15
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
thus {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4
.= {x1,x2,x3} \/ ({x4,x5} \/ {x6}) by Th3
.= ({x1,x2,x3} \/ {x4,x5}) \/ {x6} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5} \/ {x6} by Lm3 ; ::_thesis: verum
end;

Lm5:  for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5,x6,x7}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7} )
A1: ( x in {x5,x6,x7} iff ( x = x5 or x = x6 or x = x7 ) ) by Def1;
 ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2;
hence  ( x in {x1,x2,x3,x4,x5,x6,x7} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7} ) by A1, Def5, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by TARSKI:1; ::_thesis: verum
end;

theorem Th16: :: ENUMSET1:16
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7}
thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5
.= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7} by Th4
.= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4,x5,x6,x7} by Lm4 ; ::_thesis: verum
end;

theorem Th17: :: ENUMSET1:17
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7}
thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5
.= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7} by Lm2
.= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7}) by XBOOLE_1:4
.= {x1,x2} \/ {x3,x4,x5,x6,x7} by Th8 ; ::_thesis: verum
end;

theorem Th18: :: ENUMSET1:18
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7}
thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5
.= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7} by Th6
.= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7}) by XBOOLE_1:4
.= {x1,x2,x3} \/ {x4,x5,x6,x7} by Th4 ; ::_thesis: verum
end;

theorem :: ENUMSET1:19
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5;

theorem :: ENUMSET1:20
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7}
thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5
.= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7}) by Th2
.= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5} \/ {x6,x7} by Th10 ; ::_thesis: verum
end;

theorem :: ENUMSET1:21
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
thus {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5
.= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7}) by Th3
.= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6} \/ {x7} by Th14 ; ::_thesis: verum
end;

Lm6:  for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5,x6,x7,x8}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7,x8}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8} )
A1: ( x in {x5,x6,x7,x8} iff ( x = x5 or x = x6 or x = x7 or x = x8 ) ) by Def2;
 ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2;
hence  ( x in {x1,x2,x3,x4,x5,x6,x7,x8} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8} ) by A1, Def6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by TARSKI:1; ::_thesis: verum
end;

theorem :: ENUMSET1:22
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7,x8} by Th4
.= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4,x5,x6,x7,x8} by Th18 ; ::_thesis: verum
end;

theorem Th23: :: ENUMSET1:23
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7,x8} by Lm2
.= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4
.= {x1,x2} \/ {x3,x4,x5,x6,x7,x8} by Th12 ; ::_thesis: verum
end;

theorem Th24: :: ENUMSET1:24
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7,x8} by Th6
.= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7,x8}) by XBOOLE_1:4
.= {x1,x2,x3} \/ {x4,x5,x6,x7,x8} by Th7 ; ::_thesis: verum
end;

theorem :: ENUMSET1:25
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6;

theorem :: ENUMSET1:26
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7,x8}) by Th4
.= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7,x8} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5} \/ {x6,x7,x8} by Th10 ; ::_thesis: verum
end;

theorem :: ENUMSET1:27
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7,x8}) by Lm2
.= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7,x8} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6} \/ {x7,x8} by Th14 ; ::_thesis: verum
end;

theorem :: ENUMSET1:28
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}
thus {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6
.= {x1,x2,x3,x4} \/ ({x5,x6,x7} \/ {x8}) by Th6
.= ({x1,x2,x3,x4} \/ {x5,x6,x7}) \/ {x8} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6,x7} \/ {x8} by Lm5 ; ::_thesis: verum
end;

theorem Th29: :: ENUMSET1:29
for x1 being set holds {x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1} = {x1}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x1}_iff_x_in_{x1}_)
let x be set ; ::_thesis: ( x in {x1,x1} iff x in {x1} )
 ( x in {x1,x1} iff x = x1 ) by TARSKI:def_2;
hence  ( x in {x1,x1} iff x in {x1} ) by TARSKI:def_1; ::_thesis: verum
end;
hence  {x1,x1} = {x1} by TARSKI:1; ::_thesis: verum
end;

theorem Th30: :: ENUMSET1:30
for x1, x2 being set holds {x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x2} = {x1,x2}
thus {x1,x1,x2} = {x1,x1} \/ {x2} by Th3
.= {x1} \/ {x2} by Th29
.= {x1,x2} by Th1 ; ::_thesis: verum
end;

theorem Th31: :: ENUMSET1:31
for x1, x2, x3 being set holds {x1,x1,x2,x3} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x1,x2,x3} = {x1,x2,x3}
thus {x1,x1,x2,x3} = {x1,x1} \/ {x2,x3} by Lm2
.= {x1} \/ {x2,x3} by Th29
.= {x1,x2,x3} by Th2 ; ::_thesis: verum
end;

theorem Th32: :: ENUMSET1:32
for x1, x2, x3, x4 being set holds {x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
thus {x1,x1,x2,x3,x4} = {x1,x1} \/ {x2,x3,x4} by Th8
.= {x1} \/ {x2,x3,x4} by Th29
.= {x1,x2,x3,x4} by Th4 ; ::_thesis: verum
end;

theorem Th33: :: ENUMSET1:33
for x1, x2, x3, x4, x5 being set holds {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
thus {x1,x1,x2,x3,x4,x5} = {x1,x1} \/ {x2,x3,x4,x5} by Th12
.= {x1} \/ {x2,x3,x4,x5} by Th29
.= {x1,x2,x3,x4,x5} by Th7 ; ::_thesis: verum
end;

theorem Th34: :: ENUMSET1:34
for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
thus {x1,x1,x2,x3,x4,x5,x6} = {x1,x1} \/ {x2,x3,x4,x5,x6} by Th17
.= {x1} \/ {x2,x3,x4,x5,x6} by Th29
.= {x1,x2,x3,x4,x5,x6} by Th11 ; ::_thesis: verum
end;

theorem Th35: :: ENUMSET1:35
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}
thus {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x1} \/ {x2,x3,x4,x5,x6,x7} by Th23
.= {x1} \/ {x2,x3,x4,x5,x6,x7} by Th29
.= {x1,x2,x3,x4,x5,x6,x7} by Th16 ; ::_thesis: verum
end;

theorem :: ENUMSET1:36
for x1 being set holds {x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1} = {x1}
thus {x1,x1,x1} = {x1,x1} by Th30
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th37: :: ENUMSET1:37
for x1, x2 being set holds {x1,x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x1,x2} = {x1,x2}
thus {x1,x1,x1,x2} = {x1,x1,x2} by Th31
.= {x1,x2} by Th30 ; ::_thesis: verum
end;

theorem Th38: :: ENUMSET1:38
for x1, x2, x3 being set holds {x1,x1,x1,x2,x3} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x2,x3} = {x1,x2,x3}
thus {x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th32
.= {x1,x2,x3} by Th31 ; ::_thesis: verum
end;

theorem Th39: :: ENUMSET1:39
for x1, x2, x3, x4 being set holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
thus {x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th33
.= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum
end;

theorem Th40: :: ENUMSET1:40
for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
thus {x1,x1,x1,x2,x3,x4,x5} = {x1,x1,x2,x3,x4,x5} by Th34
.= {x1,x2,x3,x4,x5} by Th33 ; ::_thesis: verum
end;

theorem Th41: :: ENUMSET1:41
for x1, x2, x3, x4, x5, x6 being set holds {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
thus {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x1,x2,x3,x4,x5,x6} by Th35
.= {x1,x2,x3,x4,x5,x6} by Th34 ; ::_thesis: verum
end;

theorem :: ENUMSET1:42
for x1 being set holds {x1,x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1,x1} = {x1}
thus {x1,x1,x1,x1} = {x1,x1} by Th37
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th43: :: ENUMSET1:43
for x1, x2 being set holds {x1,x1,x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x2} = {x1,x2}
thus {x1,x1,x1,x1,x2} = {x1,x1,x2} by Th38
.= {x1,x2} by Th30 ; ::_thesis: verum
end;

theorem Th44: :: ENUMSET1:44
for x1, x2, x3 being set holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
thus {x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th39
.= {x1,x2,x3} by Th31 ; ::_thesis: verum
end;

theorem Th45: :: ENUMSET1:45
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
thus {x1,x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th40
.= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum
end;

theorem Th46: :: ENUMSET1:46
for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
thus {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x1,x2,x3,x4,x5} by Th41
.= {x1,x2,x3,x4,x5} by Th33 ; ::_thesis: verum
end;

theorem :: ENUMSET1:47
for x1 being set holds {x1,x1,x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1} = {x1}
thus {x1,x1,x1,x1,x1} = {x1,x1} by Th43
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th48: :: ENUMSET1:48
for x1, x2 being set holds {x1,x1,x1,x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2} = {x1,x2}
thus {x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th44
.= {x1,x2} by Th30 ; ::_thesis: verum
end;

theorem Th49: :: ENUMSET1:49
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
thus {x1,x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th45
.= {x1,x2,x3} by Th31 ; ::_thesis: verum
end;

theorem Th50: :: ENUMSET1:50
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
thus {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x1,x2,x3,x4} by Th46
.= {x1,x2,x3,x4} by Th32 ; ::_thesis: verum
end;

theorem :: ENUMSET1:51
for x1 being set holds {x1,x1,x1,x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1} = {x1}
thus {x1,x1,x1,x1,x1,x1} = {x1,x1} by Th48
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th52: :: ENUMSET1:52
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
thus {x1,x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th49
.= {x1,x2} by Th30 ; ::_thesis: verum
end;

theorem Th53: :: ENUMSET1:53
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
thus {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x1,x2,x3} by Th50
.= {x1,x2,x3} by Th31 ; ::_thesis: verum
end;

theorem :: ENUMSET1:54
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1} = {x1}
thus {x1,x1,x1,x1,x1,x1,x1} = {x1,x1} by Th52
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th55: :: ENUMSET1:55
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof
let x1, x2 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
thus {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x1,x2} by Th53
.= {x1,x2} by Th30 ; ::_thesis: verum
end;

theorem :: ENUMSET1:56
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
proof
let x1 be set ; ::_thesis: {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
thus {x1,x1,x1,x1,x1,x1,x1,x1} = {x1,x1} by Th55
.= {x1} by Th29 ; ::_thesis: verum
end;

theorem Th57: :: ENUMSET1:57
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x3,x2}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x1,x3,x2}
thus {x1,x2,x3} = {x1} \/ {x2,x3} by Th2
.= {x1,x3,x2} by Th2 ; ::_thesis: verum
end;

theorem Th58: :: ENUMSET1:58
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x1,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x2,x1,x3}
thus {x1,x2,x3} = {x1,x2} \/ {x3} by Th3
.= {x2,x1,x3} by Th3 ; ::_thesis: verum
end;

theorem Th59: :: ENUMSET1:59
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x3,x1}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x2,x3,x1}
thus {x1,x2,x3} = {x2,x3} \/ {x1} by Th2
.= {x2,x3,x1} by Th3 ; ::_thesis: verum
end;

theorem Th60: :: ENUMSET1:60
for x1, x2, x3 being set holds {x1,x2,x3} = {x3,x2,x1}
proof
let x1, x2, x3 be set ; ::_thesis: {x1,x2,x3} = {x3,x2,x1}
thus {x1,x2,x3} = {x3,x1,x2} by Th59
.= {x3,x2,x1} by Th57 ; ::_thesis: verum
end;

theorem Th61: :: ENUMSET1:61
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x4,x3}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x2,x4,x3}
thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4
.= {x1} \/ {x2,x4,x3} by Th57
.= {x1,x2,x4,x3} by Th4 ; ::_thesis: verum
end;

theorem :: ENUMSET1:62
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x2,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x3,x2,x4}
thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4
.= {x1} \/ {x3,x2,x4} by Th58
.= {x1,x3,x2,x4} by Th4 ; ::_thesis: verum
end;

theorem Th63: :: ENUMSET1:63
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x4,x2}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x3,x4,x2}
thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4
.= {x1} \/ {x3,x4,x2} by Th59
.= {x1,x3,x4,x2} by Th4 ; ::_thesis: verum
end;

theorem Th64: :: ENUMSET1:64
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x4,x3,x2}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x1,x4,x3,x2}
thus {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} by Th4
.= {x1} \/ {x4,x3,x2} by Th60
.= {x1,x4,x3,x2} by Th4 ; ::_thesis: verum
end;

theorem Th65: :: ENUMSET1:65
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x3,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x1,x3,x4}
thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6
.= {x2,x1,x3} \/ {x4} by Th58
.= {x2,x1,x3,x4} by Th6 ; ::_thesis: verum
end;

Lm7:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x3,x1,x4}
thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6
.= {x2,x3,x1} \/ {x4} by Th59
.= {x2,x3,x1,x4} by Th6 ; ::_thesis: verum
end;

theorem :: ENUMSET1:66
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x4,x3}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x1,x4,x3}
thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7
.= {x2,x1,x4,x3} by Th63 ; ::_thesis: verum
end;

theorem :: ENUMSET1:67
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7;

theorem :: ENUMSET1:68
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x4,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x3,x4,x1}
thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7
.= {x2,x3,x4,x1} by Th61 ; ::_thesis: verum
end;

theorem Th69: :: ENUMSET1:69
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x1,x3}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x4,x1,x3}
thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7
.= {x2,x4,x1,x3} by Th64 ; ::_thesis: verum
end;

theorem :: ENUMSET1:70
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x3,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x2,x4,x3,x1}
thus {x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7
.= {x2,x4,x3,x1} by Th63 ; ::_thesis: verum
end;

Lm8:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x2,x1,x4}
thus {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by Th6
.= {x3,x2,x1} \/ {x4} by Th60
.= {x3,x2,x1,x4} by Th6 ; ::_thesis: verum
end;

theorem :: ENUMSET1:71
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8;

theorem :: ENUMSET1:72
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x4,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x2,x4,x1}
thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8
.= {x3,x2,x4,x1} by Th61 ; ::_thesis: verum
end;

theorem :: ENUMSET1:73
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x1,x2}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x4,x1,x2}
thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8
.= {x3,x4,x1,x2} by Th64 ; ::_thesis: verum
end;

theorem Th74: :: ENUMSET1:74
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x2,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x3,x4,x2,x1}
thus {x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8
.= {x3,x4,x2,x1} by Th63 ; ::_thesis: verum
end;

theorem :: ENUMSET1:75
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x2,x3,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x4,x2,x3,x1}
thus {x1,x2,x3,x4} = {x3,x4,x2,x1} by Th74
.= {x4,x2,x3,x1} by Lm7 ; ::_thesis: verum
end;

theorem :: ENUMSET1:76
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x3,x2,x1}
proof
let x1, x2, x3, x4 be set ; ::_thesis: {x1,x2,x3,x4} = {x4,x3,x2,x1}
thus {x1,x2,x3,x4} = {x3,x4,x2,x1} by Th74
.= {x4,x3,x2,x1} by Th65 ; ::_thesis: verum
end;

Lm9:  for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9}_iff_x_in_{x1,x2,x3,x4}_\/_{x5,x6,x7,x8,x9}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} )
A1: ( x in {x5,x6,x7,x8,x9} iff ( x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Def3;
 ( x in {x1,x2,x3,x4} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) by Def2;
hence  ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff x in {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} ) by A1, Def7, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by TARSKI:1; ::_thesis: verum
end;

theorem :: ENUMSET1:77
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= ({x1} \/ {x2,x3,x4}) \/ {x5,x6,x7,x8,x9} by Th4
.= {x1} \/ ({x2,x3,x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4
.= {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9} by Th24 ; ::_thesis: verum
end;

theorem :: ENUMSET1:78
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= ({x1,x2} \/ {x3,x4}) \/ {x5,x6,x7,x8,x9} by Lm2
.= {x1,x2} \/ ({x3,x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4
.= {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9} by Th17 ; ::_thesis: verum
end;

theorem :: ENUMSET1:79
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= ({x1,x2,x3} \/ {x4}) \/ {x5,x6,x7,x8,x9} by Th6
.= {x1,x2,x3} \/ ({x4} \/ {x5,x6,x7,x8,x9}) by XBOOLE_1:4
.= {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9} by Th11 ; ::_thesis: verum
end;

theorem :: ENUMSET1:80
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9;

theorem :: ENUMSET1:81
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= {x1,x2,x3,x4} \/ ({x5} \/ {x6,x7,x8,x9}) by Th7
.= ({x1,x2,x3,x4} \/ {x5}) \/ {x6,x7,x8,x9} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9} by Th10 ; ::_thesis: verum
end;

theorem :: ENUMSET1:82
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= {x1,x2,x3,x4} \/ ({x5,x6} \/ {x7,x8,x9}) by Th8
.= ({x1,x2,x3,x4} \/ {x5,x6}) \/ {x7,x8,x9} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9} by Th14 ; ::_thesis: verum
end;

theorem :: ENUMSET1:83
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= {x1,x2,x3,x4} \/ ({x5,x6,x7} \/ {x8,x9}) by Lm3
.= ({x1,x2,x3,x4} \/ {x5,x6,x7}) \/ {x8,x9} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9} by Lm5 ; ::_thesis: verum
end;

theorem :: ENUMSET1:84
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}
thus {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9
.= {x1,x2,x3,x4} \/ ({x5,x6,x7,x8} \/ {x9}) by Th10
.= ({x1,x2,x3,x4} \/ {x5,x6,x7,x8}) \/ {x9} by XBOOLE_1:4
.= {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9} by Lm6 ; ::_thesis: verum
end;

theorem :: ENUMSET1:85
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10}
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10}
now__::_thesis:_for_x_being_set_holds_
(_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10}_iff_x_in_{x1,x2,x3,x4,x5,x6,x7,x8,x9}_\/_{x10}_)
let x be set ; ::_thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} )
A1: ( x in {x10} iff x = x10 ) by TARSKI:def_1;
 ( ( ( not x = x1 & not x = x2 & not x = x3 & not x = x4 & not x = x5 & not x = x6 & not x = x7 & not x = x8 & not x = x9 & not x = x10 ) or x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} or x = x10 ) & ( ( not x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} & not x = x10 ) or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) by Def7;
hence  ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} ) by A1, Def8, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} by TARSKI:1; ::_thesis: verum
end;

begin

theorem :: ENUMSET1:86
for x, y, z being set st x <> y & x <> z holds
{x,y,z} \ {x} = {y,z}
proof
let x, y, z be set ; ::_thesis: ( x <> y & x <> z implies {x,y,z} \ {x} = {y,z} )
assume A1: ( x <> y & x <> z ) ; ::_thesis: {x,y,z} \ {x} = {y,z}
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y,z} c= {x,y,z} \ {x}
let a be set ; ::_thesis: ( a in {x,y,z} \ {x} implies a in {y,z} )
assume A2: a in {x,y,z} \ {x} ; ::_thesis: a in {y,z}
then  a in {x,y,z} by XBOOLE_0:def_5;
then A3: ( a = x or a = y or a = z ) by Def1;
 not a in {x} by A2, XBOOLE_0:def_5;
hence  a in {y,z} by A3, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {y,z} or a in {x,y,z} \ {x} )
assume  a in {y,z} ; ::_thesis: a in {x,y,z} \ {x}
then A4: ( a = y or a = z ) by TARSKI:def_2;
then A5: not a in {x} by A1, TARSKI:def_1;
 a in {x,y,z} by A4, Def1;
hence  a in {x,y,z} \ {x} by A5, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: ENUMSET1:87
for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}
proof
let x1, x2, x3 be set ; ::_thesis: {x2,x1} \/ {x3,x1} = {x1,x2,x3}
thus {x2,x1} \/ {x3,x1} = {x2,x1,x3,x1} by Lm2
.= {x1,x1,x2,x3} by Th69
.= {x1,x2,x3} by Th31 ; ::_thesis: verum
end;