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


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

definition
let x1, x2, x3 be object ;
func {x1,x2,x3} -> set means :Def1: :: ENUMSET1:def 1
 for x being object holds
( x in it iff ( x = x1 or x = x2 or x = x3 ) );
existence
ex b1 being set st
for x being object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being object holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b1 = b2
proof end;
end;

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

definition
let x1, x2, x3, x4 be object ;
func {x1,x2,x3,x4} -> set means :Def2: :: ENUMSET1:def 2
 for x being object 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 object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being object holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b1 = b2
proof end;
end;

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

definition
let x1, x2, x3, x4, x5 be object ;
func {x1,x2,x3,x4,x5} -> set means :Def3: :: ENUMSET1:def 3
 for x being object 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 object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being object holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :
for x1, x2, x3, x4, x5 being object
for b6 being set holds
( b6 = {x1,x2,x3,x4,x5} iff for x being object 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 object ;
func {x1,x2,x3,x4,x5,x6} -> set means :Def4: :: ENUMSET1:def 4
 for x being object 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 object holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 end;
end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :
for x1, x2, x3, x4, x5, x6 being object
for b7 being set holds
( b7 = {x1,x2,x3,x4,x5,x6} iff for x being object 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 object ;
func {x1,x2,x3,x4,x5,x6,x7} -> set means :Def5: :: ENUMSET1:def 5
 for x being object 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 object 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 end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 end;
end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :
for x1, x2, x3, x4, x5, x6, x7 being object
for b8 being set holds
( b8 = {x1,x2,x3,x4,x5,x6,x7} iff for x being object 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 object ;
func {x1,x2,x3,x4,x5,x6,x7,x8} -> set means :Def6: :: ENUMSET1:def 6
 for x being object 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 object 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 end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 end;
end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :
for x1, x2, x3, x4, x5, x6, x7, x8 being object
for b9 being set holds
( b9 = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being object 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 object ;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> set means :Def7: :: ENUMSET1:def 7
 for x being object 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 object 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 end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 end;
end;

:: deftheorem Def7 defines { ENUMSET1:def 7 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object
for b10 being set holds
( b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being object 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 object ;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> set means :Def8: :: ENUMSET1:def 8
 for x being object 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 object 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 end;
uniqueness
for b1, b2 being set st ( for x being object 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 object 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 end;
end;

:: deftheorem Def8 defines { ENUMSET1:def 8 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being object
for b11 being set holds
( b11 = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being object 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 object holds {x1,x2} = {x1} \/ {x2}
proof end;

theorem Th2: :: ENUMSET1:2
for x1, x2, x3 being object holds {x1,x2,x3} = {x1} \/ {x2,x3}
proof end;

theorem Th3: :: ENUMSET1:3
for x1, x2, x3 being object holds {x1,x2,x3} = {x1,x2} \/ {x3}
proof end;

Lm2: for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
proof end;

theorem Th4: :: ENUMSET1:4
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
proof end;

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

theorem Th6: :: ENUMSET1:6
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
proof end;

Lm3: for x1, x2, x3, x4, x5 being object holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
proof end;

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

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

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

theorem Th10: :: ENUMSET1:10
for x1, x2, x3, x4, x5 being object holds {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
proof end;

Lm4: for x1, x2, x3, x4, x5, x6 being object holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
proof end;

theorem Th11: :: ENUMSET1:11
for x1, x2, x3, x4, x5, x6 being object holds {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}
proof end;

theorem Th12: :: ENUMSET1:12
for x1, x2, x3, x4, x5, x6 being object holds {x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}
proof end;

theorem :: ENUMSET1:13
for x1, x2, x3, x4, x5, x6 being object 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 object holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}
proof end;

theorem :: ENUMSET1:15
for x1, x2, x3, x4, x5, x6 being object holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
proof end;

Lm5: for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}
proof end;

theorem Th16: :: ENUMSET1:16
for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7}
proof end;

theorem Th17: :: ENUMSET1:17
for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7}
proof end;

theorem Th18: :: ENUMSET1:18
for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7}
proof end;

theorem :: ENUMSET1:19
for x1, x2, x3, x4, x5, x6, x7 being object 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 object holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7}
proof end;

theorem :: ENUMSET1:21
for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
proof end;

Lm6: for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}
proof end;

theorem :: ENUMSET1:22
for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}
proof end;

theorem Th23: :: ENUMSET1:23
for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}
proof end;

theorem Th24: :: ENUMSET1:24
for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}
proof end;

theorem :: ENUMSET1:25
for x1, x2, x3, x4, x5, x6, x7, x8 being object 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 object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}
proof end;

theorem :: ENUMSET1:27
for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}
proof end;

theorem :: ENUMSET1:28
for x1, x2, x3, x4, x5, x6, x7, x8 being object holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}
proof end;

theorem Th29: :: ENUMSET1:29
for x1 being object holds {x1,x1} = {x1}
proof end;

theorem Th30: :: ENUMSET1:30
for x1, x2 being object holds {x1,x1,x2} = {x1,x2}
proof end;

theorem Th31: :: ENUMSET1:31
for x1, x2, x3 being object holds {x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th32: :: ENUMSET1:32
for x1, x2, x3, x4 being object holds {x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem Th33: :: ENUMSET1:33
for x1, x2, x3, x4, x5 being object holds {x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof end;

theorem Th34: :: ENUMSET1:34
for x1, x2, x3, x4, x5, x6 being object holds {x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
proof end;

theorem Th35: :: ENUMSET1:35
for x1, x2, x3, x4, x5, x6, x7 being object holds {x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}
proof end;

theorem :: ENUMSET1:36
for x1 being object holds {x1,x1,x1} = {x1}
proof end;

theorem Th37: :: ENUMSET1:37
for x1, x2 being object holds {x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th38: :: ENUMSET1:38
for x1, x2, x3 being object holds {x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th39: :: ENUMSET1:39
for x1, x2, x3, x4 being object holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem Th40: :: ENUMSET1:40
for x1, x2, x3, x4, x5 being object holds {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof end;

theorem Th41: :: ENUMSET1:41
for x1, x2, x3, x4, x5, x6 being object holds {x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
proof end;

theorem :: ENUMSET1:42
for x1 being object holds {x1,x1,x1,x1} = {x1}
proof end;

theorem Th43: :: ENUMSET1:43
for x1, x2 being object holds {x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th44: :: ENUMSET1:44
for x1, x2, x3 being object holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th45: :: ENUMSET1:45
for x1, x2, x3, x4 being object holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem Th46: :: ENUMSET1:46
for x1, x2, x3, x4, x5 being object holds {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof end;

theorem :: ENUMSET1:47
for x1 being object holds {x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th48: :: ENUMSET1:48
for x1, x2 being object holds {x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th49: :: ENUMSET1:49
for x1, x2, x3 being object holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th50: :: ENUMSET1:50
for x1, x2, x3, x4 being object holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem :: ENUMSET1:51
for x1 being object holds {x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th52: :: ENUMSET1:52
for x1, x2 being object holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th53: :: ENUMSET1:53
for x1, x2, x3 being object holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem :: ENUMSET1:54
for x1 being object holds {x1,x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th55: :: ENUMSET1:55
for x1, x2 being object holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem :: ENUMSET1:56
for x1 being object holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th57: :: ENUMSET1:57
for x1, x2, x3 being object holds {x1,x2,x3} = {x1,x3,x2}
proof end;

theorem Th58: :: ENUMSET1:58
for x1, x2, x3 being object holds {x1,x2,x3} = {x2,x1,x3}
proof end;

theorem Th59: :: ENUMSET1:59
for x1, x2, x3 being object holds {x1,x2,x3} = {x2,x3,x1}
proof end;

theorem Th60: :: ENUMSET1:60
for x1, x2, x3 being object holds {x1,x2,x3} = {x3,x2,x1}
proof end;

theorem Th61: :: ENUMSET1:61
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x2,x4,x3}
proof end;

theorem :: ENUMSET1:62
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x3,x2,x4}
proof end;

theorem Th63: :: ENUMSET1:63
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x3,x4,x2}
proof end;

theorem Th64: :: ENUMSET1:64
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x1,x4,x3,x2}
proof end;

theorem Th65: :: ENUMSET1:65
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x1,x3,x4}
proof end;

Lm7: for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x3,x1,x4}
proof end;

theorem :: ENUMSET1:66
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x1,x4,x3}
proof end;

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

theorem :: ENUMSET1:68
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x3,x4,x1}
proof end;

theorem Th69: :: ENUMSET1:69
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x4,x1,x3}
proof end;

theorem :: ENUMSET1:70
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x2,x4,x3,x1}
proof end;

Lm8: for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x3,x2,x1,x4}
proof end;

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

theorem :: ENUMSET1:72
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x3,x2,x4,x1}
proof end;

theorem :: ENUMSET1:73
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x3,x4,x1,x2}
proof end;

theorem Th74: :: ENUMSET1:74
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x3,x4,x2,x1}
proof end;

theorem :: ENUMSET1:75
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x4,x2,x3,x1}
proof end;

theorem :: ENUMSET1:76
for x1, x2, x3, x4 being object holds {x1,x2,x3,x4} = {x4,x3,x2,x1}
proof end;

Lm9: for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
proof end;

theorem :: ENUMSET1:77
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}
proof end;

theorem :: ENUMSET1:78
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}
proof end;

theorem :: ENUMSET1:79
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}
proof end;

theorem :: ENUMSET1:80
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object 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 object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}
proof end;

theorem :: ENUMSET1:82
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}
proof end;

theorem :: ENUMSET1:83
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}
proof end;

theorem :: ENUMSET1:84
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}
proof end;

theorem :: ENUMSET1:85
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10}
proof end;

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

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