:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990-2011 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 b₁ being set st
for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds
( x in b₂ iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines { ENUMSET1:def 1 :
for x1, x2, x3, b₄ being set holds
( b₄ = {x1,x2,x3} iff for x being set holds
( x in b₄ 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 b₁ being set st
for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds
( x in b₂ iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines { ENUMSET1:def 2 :
for x1, x2, x3, x4, b₅ being set holds
( b₅ = {x1,x2,x3,x4} iff for x being set holds
( x in b₅ 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 b₁ being set st
for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds
( x in b₂ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :
for x1, x2, x3, x4, x5, b₆ being set holds
( b₆ = {x1,x2,x3,x4,x5} iff for x being set holds
( x in b₆ 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 b₁ being set st
for x being set holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ 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 b₂ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :
for x1, x2, x3, x4, x5, x6, b₇ being set holds
( b₇ = {x1,x2,x3,x4,x5,x6} iff for x being set holds
( x in b₇ 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 b₁ being set st
for x being set holds
( x in b₁ 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 b₁, b₂ being set st ( for x being set holds
( x in b₁ 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 b₂ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :
for x1, x2, x3, x4, x5, x6, x7, b₈ being set holds
( b₈ = {x1,x2,x3,x4,x5,x6,x7} iff for x being set holds
( x in b₈ 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 b₁ being set st
for x being set holds
( x in b₁ 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 b₁, b₂ being set st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :
for x1, x2, x3, x4, x5, x6, x7, x8, b₉ being set holds
( b₉ = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being set holds
( x in b₉ 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 b₁ being set st
for x being set holds
( x in b₁ 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 b₁, b₂ being set st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines { ENUMSET1:def 7 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, b₁₀ being set holds
( b₁₀ = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds
( x in b₁₀ 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 b₁ being set st
for x being set holds
( x in b₁ 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 b₁, b₂ being set st ( for x being set holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

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