:: 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 b_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 ) ) ) holds

b_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines { ENUMSET1:def 1 :

for x1, x2, x3, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds

b_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines { ENUMSET1:def 2 :

for x1, x2, x3, x4, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds

( x in b_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds

b_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines { ENUMSET1:def 3 :

for x1, x2, x3, x4, x5, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds

b_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def4 defines { ENUMSET1:def 4 :

for x1, x2, x3, x4, x5, x6, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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_{2} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds

b_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines { ENUMSET1:def 5 :

for x1, x2, x3, x4, x5, x6, x7, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines { ENUMSET1:def 6 :

for x1, x2, x3, x4, x5, x6, x7, x8, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines { ENUMSET1:def 7 :

for x1, x2, x3, x4, x5, x6, x7, x8, x9, b

( b

( x in b

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_{1} being set st

for x being set holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines { ENUMSET1:def 8 :

for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b

( b

( x in b

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

proof end;

theorem Th42: :: ENUMSET1:42

proof end;

theorem Th43: :: ENUMSET1:43

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

proof end;

theorem :: ENUMSET1:45

theorem Th46: :: ENUMSET1:46

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

proof end;

theorem Th48: :: ENUMSET1:48

proof end;

theorem :: ENUMSET1:49

theorem Th50: :: ENUMSET1:50

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

proof end;

theorem Th52: :: ENUMSET1:52

proof end;

theorem :: ENUMSET1:53

theorem Th54: :: ENUMSET1:54

proof end;

theorem :: ENUMSET1:55

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

proof end;

theorem Th57: :: ENUMSET1:57

proof end;

theorem Th58: :: ENUMSET1:58

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

proof end;

theorem :: ENUMSET1:61

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

proof end;

theorem Th70: :: ENUMSET1:70

proof end;

theorem Th71: :: ENUMSET1:71

proof end;

theorem Th72: :: ENUMSET1:72

proof end;

theorem Th73: :: ENUMSET1:73

proof end;

theorem Th74: :: ENUMSET1:74

proof end;

theorem Th75: :: ENUMSET1:75

proof end;

theorem :: ENUMSET1:76

proof end;

theorem Th77: :: ENUMSET1:77

proof end;

theorem Th78: :: ENUMSET1:78

proof end;

theorem Th79: :: ENUMSET1:79

proof end;

theorem Th80: :: ENUMSET1:80

proof end;

theorem Th81: :: ENUMSET1:81

proof end;

theorem :: ENUMSET1:82

proof end;

theorem Th83: :: ENUMSET1:83

proof end;

theorem Th84: :: ENUMSET1:84

proof end;

theorem Th85: :: ENUMSET1:85

proof end;

theorem Th86: :: ENUMSET1:86

proof end;

theorem :: ENUMSET1:87

proof end;

theorem Th88: :: ENUMSET1:88

proof end;

theorem Th89: :: ENUMSET1:89

proof end;

theorem Th90: :: ENUMSET1:90

proof end;

theorem :: ENUMSET1:91

proof end;

theorem Th92: :: ENUMSET1:92

proof end;

theorem Th93: :: ENUMSET1:93

proof end;

theorem :: ENUMSET1:94

proof end;

theorem Th95: :: ENUMSET1:95

proof end;

theorem :: ENUMSET1:96

proof end;

theorem :: ENUMSET1:97

canceled;

theorem Th98: :: ENUMSET1:98

proof end;

theorem Th99: :: ENUMSET1:99

proof end;

theorem Th100: :: ENUMSET1:100

proof end;

theorem :: ENUMSET1:101

canceled;

theorem Th102: :: ENUMSET1:102

proof end;

theorem Th103: :: ENUMSET1:103

proof end;

theorem :: ENUMSET1:104

proof end;

theorem Th105: :: ENUMSET1:105

proof end;

theorem :: ENUMSET1:106

canceled;

theorem Th107: :: ENUMSET1:107

proof end;

theorem Th108: :: ENUMSET1:108

proof end;

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

proof end;

theorem :: ENUMSET1:109

proof end;

theorem :: ENUMSET1:110

theorem :: ENUMSET1:111

proof end;

theorem Th112: :: ENUMSET1:112

proof end;

theorem :: ENUMSET1:113

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

theorem :: ENUMSET1:117

proof end;

theorem :: ENUMSET1:118

proof end;

theorem Th119: :: ENUMSET1:119

proof end;

theorem :: ENUMSET1:120

canceled;

theorem :: ENUMSET1:121

canceled;

theorem :: ENUMSET1:122

canceled;

theorem :: ENUMSET1:123

proof end;

theorem :: ENUMSET1:124

canceled;

theorem :: ENUMSET1:125

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

proof end;

theorem :: ENUMSET1:137

proof end;