:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990 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 ) )
proof 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 :: ENUMSET1:1
canceled;

theorem :: ENUMSET1:2
canceled;

theorem :: ENUMSET1:3
canceled;

theorem :: ENUMSET1:4
canceled;

theorem :: ENUMSET1:5
canceled;

theorem :: ENUMSET1:6
canceled;

theorem :: ENUMSET1:7
canceled;

theorem :: ENUMSET1:8
canceled;

theorem :: ENUMSET1:9
canceled;

theorem :: ENUMSET1:10
canceled;

theorem :: ENUMSET1:11
canceled;

theorem :: ENUMSET1:12
canceled;

theorem :: ENUMSET1:13
canceled;

theorem :: ENUMSET1:14
canceled;

theorem :: ENUMSET1:15
canceled;

theorem :: ENUMSET1:16
canceled;

theorem :: ENUMSET1:17
canceled;

theorem :: ENUMSET1:18
canceled;

theorem :: ENUMSET1:19
canceled;

theorem :: ENUMSET1:20
canceled;

theorem :: ENUMSET1:21
canceled;

theorem :: ENUMSET1:22
canceled;

theorem :: ENUMSET1:23
canceled;

theorem :: ENUMSET1:24
canceled;

theorem :: ENUMSET1:25
canceled;

theorem :: ENUMSET1:26
canceled;

theorem :: ENUMSET1:27
canceled;

theorem :: ENUMSET1:28
canceled;

theorem :: ENUMSET1:29
canceled;

theorem :: ENUMSET1:30
canceled;

theorem :: ENUMSET1:31
canceled;

theorem :: ENUMSET1:32
canceled;

theorem :: ENUMSET1:33
canceled;

theorem :: ENUMSET1:34
canceled;

theorem :: ENUMSET1:35
canceled;

theorem :: ENUMSET1:36
canceled;

theorem :: ENUMSET1:37
canceled;

theorem :: ENUMSET1:38
canceled;

theorem :: ENUMSET1:39
canceled;

theorem :: ENUMSET1:40
canceled;

theorem Th41: :: ENUMSET1:41
for x1, x2 being set holds {x1,x2} = {x1} \/ {x2}
proof end;

theorem Th42: :: ENUMSET1:42
for x1, x2, x3 being set holds {x1,x2,x3} = {x1} \/ {x2,x3}
proof end;

theorem Th43: :: ENUMSET1:43
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x2} \/ {x3}
proof end;

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

theorem Th44: :: ENUMSET1:44
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
proof end;

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

theorem Th46: :: ENUMSET1:46
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
proof end;

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

theorem Th47: :: ENUMSET1:47
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
proof end;

theorem Th48: :: ENUMSET1:48
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
proof end;

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

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

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

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

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

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

theorem Th56: :: ENUMSET1:56
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 end;

theorem Th57: :: ENUMSET1:57
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 end;

theorem Th58: :: ENUMSET1:58
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 end;

theorem :: ENUMSET1:59
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:60
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 end;

theorem :: ENUMSET1:61
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 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 end;

theorem :: ENUMSET1:62
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 end;

theorem Th63: :: ENUMSET1:63
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 end;

theorem Th64: :: ENUMSET1:64
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 end;

theorem :: ENUMSET1:65
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:66
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 end;

theorem :: ENUMSET1:67
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 end;

theorem :: ENUMSET1:68
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 end;

theorem Th69: :: ENUMSET1:69
for x1 being set holds {x1,x1} = {x1}
proof end;

theorem Th70: :: ENUMSET1:70
for x1, x2 being set holds {x1,x1,x2} = {x1,x2}
proof end;

theorem Th71: :: ENUMSET1:71
for x1, x2, x3 being set holds {x1,x1,x2,x3} = {x1,x2,x3}
proof end;

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

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

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

theorem Th75: :: ENUMSET1:75
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 end;

theorem :: ENUMSET1:76
for x1 being set holds {x1,x1,x1} = {x1}
proof end;

theorem Th77: :: ENUMSET1:77
for x1, x2 being set holds {x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th78: :: ENUMSET1:78
for x1, x2, x3 being set holds {x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th79: :: ENUMSET1:79
for x1, x2, x3, x4 being set holds {x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem Th80: :: ENUMSET1:80
for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof end;

theorem Th81: :: ENUMSET1:81
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 end;

theorem :: ENUMSET1:82
for x1 being set holds {x1,x1,x1,x1} = {x1}
proof end;

theorem Th83: :: ENUMSET1:83
for x1, x2 being set holds {x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th84: :: ENUMSET1:84
for x1, x2, x3 being set holds {x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th85: :: ENUMSET1:85
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem Th86: :: ENUMSET1:86
for x1, x2, x3, x4, x5 being set holds {x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
proof end;

theorem :: ENUMSET1:87
for x1 being set holds {x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th88: :: ENUMSET1:88
for x1, x2 being set holds {x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th89: :: ENUMSET1:89
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem Th90: :: ENUMSET1:90
for x1, x2, x3, x4 being set holds {x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
proof end;

theorem :: ENUMSET1:91
for x1 being set holds {x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th92: :: ENUMSET1:92
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem Th93: :: ENUMSET1:93
for x1, x2, x3 being set holds {x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
proof end;

theorem :: ENUMSET1:94
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem Th95: :: ENUMSET1:95
for x1, x2 being set holds {x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
proof end;

theorem :: ENUMSET1:96
for x1 being set holds {x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
proof end;

theorem :: ENUMSET1:97
canceled;

theorem Th98: :: ENUMSET1:98
for x1, x2, x3 being set holds {x1,x2,x3} = {x1,x3,x2}
proof end;

theorem Th99: :: ENUMSET1:99
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x1,x3}
proof end;

theorem Th100: :: ENUMSET1:100
for x1, x2, x3 being set holds {x1,x2,x3} = {x2,x3,x1}
proof end;

theorem :: ENUMSET1:101
canceled;

theorem Th102: :: ENUMSET1:102
for x1, x2, x3 being set holds {x1,x2,x3} = {x3,x2,x1}
proof end;

theorem Th103: :: ENUMSET1:103
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2,x4,x3}
proof end;

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

theorem Th105: :: ENUMSET1:105
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x3,x4,x2}
proof end;

theorem :: ENUMSET1:106
canceled;

theorem Th107: :: ENUMSET1:107
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x4,x3,x2}
proof end;

theorem Th108: :: ENUMSET1:108
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x1,x3,x4}
proof end;

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

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

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

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

theorem Th112: :: ENUMSET1:112
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x4,x1,x3}
proof end;

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

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

theorem :: ENUMSET1:114
canceled;

theorem :: ENUMSET1:115
canceled;

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

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

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

theorem Th119: :: ENUMSET1:119
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x4,x2,x1}
proof end;

theorem :: ENUMSET1:120
canceled;

theorem :: ENUMSET1:121
canceled;

theorem :: ENUMSET1:122
canceled;

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

theorem :: ENUMSET1:124
canceled;

theorem :: ENUMSET1:125
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x4,x3,x2,x1}
proof 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 end;

theorem :: ENUMSET1:126
canceled;

theorem :: ENUMSET1:127
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 end;

theorem :: ENUMSET1:128
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 end;

theorem :: ENUMSET1:129
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 end;

theorem :: ENUMSET1:130
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:131
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 end;

theorem :: ENUMSET1:132
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 end;

theorem :: ENUMSET1:133
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 end;

theorem :: ENUMSET1:134
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 end;

theorem :: ENUMSET1:135
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 end;

begin

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

theorem :: ENUMSET1:137
for x1, x2, x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3}
proof end;