:: Enumerated Sets
:: by Andrzej Trybulec
::
:: Received January 8, 1989
:: Copyright (c) 1990-2021 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 b₁ being set st
for x being object 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 object holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being object 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 being object
for b₄ being set holds
( b₄ = {x1,x2,x3} iff for x being object holds
( x in b₄ 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 b₁ being set st
for x being object 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 object holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being object 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 being object
for b₅ being set holds
( b₅ = {x1,x2,x3,x4} iff for x being object holds
( x in b₅ 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 b₁ being set st
for x being object 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 object holds
( x in b₁ iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being object 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 being object
for b₆ being set holds
( b₆ = {x1,x2,x3,x4,x5} iff for x being object 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 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 b₁ being set st
for x being object 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 object 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 object 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 being object
for b₇ being set holds
( b₇ = {x1,x2,x3,x4,x5,x6} iff for x being object 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 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 b₁ being set st
for x being object 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 object 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 object 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 being object
for b₈ being set holds
( b₈ = {x1,x2,x3,x4,x5,x6,x7} iff for x being object 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 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 b₁ being set st
for x being object 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 object 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 object 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 being object
for b₉ being set holds
( b₉ = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being object 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 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 b₁ being set st
for x being object 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 object 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 object 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 being object
for b₁₀ being set holds
( b₁₀ = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being object 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 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 b₁ being set st
for x being object 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 object 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 object 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 being object
for b₁₁ being set holds
( b₁₁ = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being object 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 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;