:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1:  for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
proofend;

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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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 ) )
proofend;
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
proofend;
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}
proofend;

theorem Th2: :: ENUMSET1:2
for x1, x2, x3 being set holds {x1,x2,x3} = {x1} \/ {x2,x3}
proofend;

theorem Th3: :: ENUMSET1:3
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x2} \/ {x3}
proofend;

Lm2:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
proofend;

theorem Th4: :: ENUMSET1:4
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
proofend;

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}
proofend;

Lm3:  for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
proofend;

theorem Th7: :: ENUMSET1:7
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
proofend;

theorem Th8: :: ENUMSET1:8
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
proofend;

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}
proofend;

Lm4:  for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

theorem Th29: :: ENUMSET1:29
for x1 being set holds {x1,x1} = {x1}
proofend;

theorem Th30: :: ENUMSET1:30
for x1, x2 being set holds {x1,x1,x2} = {x1,x2}
proofend;

theorem Th31: :: ENUMSET1:31
for x1, x2, x3 being set holds {x1,x1,x2,x3} = {x1,x2,x3}
proofend;

theorem Th32: :: ENUMSET1:32
for x1, x2, x3, x4 being set holds {x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proofend;

theorem Th33: :: ENUMSET1:33
for x1, x2, x3, x4, x5 being set holds {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proofend;

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}
proofend;

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}
proofend;

theorem :: ENUMSET1:36
for x1 being set holds {x1,x1,x1} = {x1}
proofend;

theorem Th37: :: ENUMSET1:37
for x1, x2 being set holds {x1,x1,x1,x2} = {x1,x2}
proofend;

theorem Th38: :: ENUMSET1:38
for x1, x2, x3 being set holds {x1,x1,x1,x2,x3} = {x1,x2,x3}
proofend;

theorem Th39: :: ENUMSET1:39
for x1, x2, x3, x4 being set holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proofend;

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}
proofend;

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}
proofend;

theorem :: ENUMSET1:42
for x1 being set holds {x1,x1,x1,x1} = {x1}
proofend;

theorem Th43: :: ENUMSET1:43
for x1, x2 being set holds {x1,x1,x1,x1,x2} = {x1,x2}
proofend;

theorem Th44: :: ENUMSET1:44
for x1, x2, x3 being set holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proofend;

theorem Th45: :: ENUMSET1:45
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proofend;

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}
proofend;

theorem :: ENUMSET1:47
for x1 being set holds {x1,x1,x1,x1,x1} = {x1}
proofend;

theorem Th48: :: ENUMSET1:48
for x1, x2 being set holds {x1,x1,x1,x1,x1,x2} = {x1,x2}
proofend;

theorem Th49: :: ENUMSET1:49
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proofend;

theorem Th50: :: ENUMSET1:50
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proofend;

theorem :: ENUMSET1:51
for x1 being set holds {x1,x1,x1,x1,x1,x1} = {x1}
proofend;

theorem Th52: :: ENUMSET1:52
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proofend;

theorem Th53: :: ENUMSET1:53
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proofend;

theorem :: ENUMSET1:54
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1} = {x1}
proofend;

theorem Th55: :: ENUMSET1:55
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proofend;

theorem :: ENUMSET1:56
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
proofend;

theorem Th57: :: ENUMSET1:57
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x3,x2}
proofend;

theorem Th58: :: ENUMSET1:58
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x1,x3}
proofend;

theorem Th59: :: ENUMSET1:59
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x3,x1}
proofend;

theorem Th60: :: ENUMSET1:60
for x1, x2, x3 being set holds {x1,x2,x3} = {x3,x2,x1}
proofend;

theorem Th61: :: ENUMSET1:61
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x4,x3}
proofend;

theorem :: ENUMSET1:62
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x2,x4}
proofend;

theorem Th63: :: ENUMSET1:63
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x4,x2}
proofend;

theorem Th64: :: ENUMSET1:64
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x4,x3,x2}
proofend;

theorem Th65: :: ENUMSET1:65
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x3,x4}
proofend;

Lm7:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}
proofend;

theorem :: ENUMSET1:66
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x4,x3}
proofend;

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}
proofend;

theorem Th69: :: ENUMSET1:69
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x1,x3}
proofend;

theorem :: ENUMSET1:70
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x3,x1}
proofend;

Lm8:  for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}
proofend;

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}
proofend;

theorem :: ENUMSET1:73
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x1,x2}
proofend;

theorem Th74: :: ENUMSET1:74
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x2,x1}
proofend;

theorem :: ENUMSET1:75
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x2,x3,x1}
proofend;

theorem :: ENUMSET1:76
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x3,x2,x1}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

begin

theorem :: ENUMSET1:86
for x, y, z being set st x <> y &amp; x <> z holds
{x,y,z} \ {x} = {y,z}
proofend;

:: from SCMBSORT, 2007.07.26, A.T.
theorem :: ENUMSET1:87
for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}
proofend;