:: by Zinaida Trybulec

::

:: Received March 4, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

registration
end;

registration

let x1, x2, x3 be set ;

cluster {x1,x2,x3} -> non empty ;

coherence

not {x1,x2,x3} is empty by ENUMSET1:def 1;

let x4 be set ;

cluster {x1,x2,x3,x4} -> non empty ;

coherence

not {x1,x2,x3,x4} is empty by ENUMSET1:def 2;

let x5 be set ;

cluster {x1,x2,x3,x4,x5} -> non empty ;

coherence

not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def 3;

let x6 be set ;

cluster {x1,x2,x3,x4,x5,x6} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def 4;

let x7 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def 5;

let x8 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def 6;

let x9 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def 7;

let x10 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def 8;

end;
cluster {x1,x2,x3} -> non empty ;

coherence

not {x1,x2,x3} is empty by ENUMSET1:def 1;

let x4 be set ;

cluster {x1,x2,x3,x4} -> non empty ;

coherence

not {x1,x2,x3,x4} is empty by ENUMSET1:def 2;

let x5 be set ;

cluster {x1,x2,x3,x4,x5} -> non empty ;

coherence

not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def 3;

let x6 be set ;

cluster {x1,x2,x3,x4,x5,x6} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def 4;

let x7 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def 5;

let x8 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def 6;

let x9 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def 7;

let x10 be set ;

cluster {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> non empty ;

coherence

not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def 8;

definition

let X be set ;

canceled;

mode Element of X -> set means :Def2: :: SUBSET_1:def 2

it in X if not X is empty

otherwise it is empty ;

existence

( ( not X is empty implies ex b_{1} being set st b_{1} in X ) & ( X is empty implies ex b_{1} being set st b_{1} is empty ) )
by XBOOLE_0:def 1;

consistency

for b_{1} being set holds verum
;

end;
canceled;

mode Element of X -> set means :Def2: :: SUBSET_1:def 2

it in X if not X is empty

otherwise it is empty ;

existence

( ( not X is empty implies ex b

consistency

for b

:: deftheorem SUBSET_1:def 1 :

canceled;

:: deftheorem Def2 defines Element SUBSET_1:def 2 :

for X being set

for b

( ( not X is empty implies ( b

registration

let X be non empty set ;

cluster non empty Element of bool X;

existence

not for b_{1} being Subset of X holds b_{1} is empty

end;
cluster non empty Element of bool X;

existence

not for b

proof end;

registration

let X1, X2 be non empty set ;

cluster [:X1,X2:] -> non empty ;

coherence

not [:X1,X2:] is empty

end;
cluster [:X1,X2:] -> non empty ;

coherence

not [:X1,X2:] is empty

proof end;

registration

let X1, X2, X3 be non empty set ;

cluster [:X1,X2,X3:] -> non empty ;

coherence

not [:X1,X2,X3:] is empty

end;
cluster [:X1,X2,X3:] -> non empty ;

coherence

not [:X1,X2,X3:] is empty

proof end;

registration

let X1, X2, X3, X4 be non empty set ;

cluster [:X1,X2,X3,X4:] -> non empty ;

coherence

not [:X1,X2,X3,X4:] is empty

end;
cluster [:X1,X2,X3,X4:] -> non empty ;

coherence

not [:X1,X2,X3,X4:] is empty

proof end;

definition

let D be non empty set ;

let X be non empty Subset of D;

:: original: Element

redefine mode Element of X -> Element of D;

coherence

for b_{1} being Element of X holds b_{1} is Element of D

end;
let X be non empty Subset of D;

:: original: Element

redefine mode Element of X -> Element of D;

coherence

for b

proof end;

Lm1: for E being set

for X being Subset of E

for x being set st x in X holds

x in E

proof end;

registration

let E be set ;

cluster empty Element of bool E;

existence

ex b_{1} being Subset of E st b_{1} is empty

end;
cluster empty Element of bool E;

existence

ex b

proof end;

definition

let E be set ;

func {} E -> Subset of E equals :: SUBSET_1:def 3

{} ;

coherence

{} is Subset of E

;

func [#] E -> Subset of E equals :: SUBSET_1:def 4

E;

coherence

E is Subset of E

;

end;
func {} E -> Subset of E equals :: SUBSET_1:def 3

{} ;

coherence

{} is Subset of E

proof end;

correctness ;

func [#] E -> Subset of E equals :: SUBSET_1:def 4

E;

coherence

E is Subset of E

proof end;

correctness ;

:: deftheorem defines {} SUBSET_1:def 3 :

for E being set holds {} E = {} ;

:: deftheorem defines [#] SUBSET_1:def 4 :

for E being set holds [#] E = E;

theorem :: SUBSET_1:1

canceled;

theorem :: SUBSET_1:2

canceled;

theorem :: SUBSET_1:3

canceled;

theorem :: SUBSET_1:4

proof end;

theorem :: SUBSET_1:5

canceled;

theorem :: SUBSET_1:6

canceled;

theorem Th7: :: SUBSET_1:7

for E being set

for A, B being Subset of E st ( for x being Element of E st x in A holds

x in B ) holds

A c= B

for A, B being Subset of E st ( for x being Element of E st x in A holds

x in B ) holds

A c= B

proof end;

theorem Th8: :: SUBSET_1:8

for E being set

for A, B being Subset of E st ( for x being Element of E holds

( x in A iff x in B ) ) holds

A = B

for A, B being Subset of E st ( for x being Element of E holds

( x in A iff x in B ) ) holds

A = B

proof end;

theorem :: SUBSET_1:9

canceled;

theorem :: SUBSET_1:10

proof end;

definition

let E be set ;

let A be Subset of E;

func A ` -> Subset of E equals :: SUBSET_1:def 5

E \ A;

coherence

E \ A is Subset of E

;

involutiveness

for b_{1}, b_{2} being Subset of E st b_{1} = E \ b_{2} holds

b_{2} = E \ b_{1}

:: original: \/

redefine func A \/ B -> Subset of E;

coherence

A \/ B is Subset of E

redefine func A \+\ B -> Subset of E;

coherence

A \+\ B is Subset of E

end;
let A be Subset of E;

func A ` -> Subset of E equals :: SUBSET_1:def 5

E \ A;

coherence

E \ A is Subset of E

proof end;

correctness ;

involutiveness

for b

b

proof end;

let B be Subset of E;:: original: \/

redefine func A \/ B -> Subset of E;

coherence

A \/ B is Subset of E

proof end;

:: original: \+\redefine func A \+\ B -> Subset of E;

coherence

A \+\ B is Subset of E

proof end;

:: deftheorem defines ` SUBSET_1:def 5 :

for E being set

for A being Subset of E holds A ` = E \ A;

definition

let X, Y be set ;

:: original: \

redefine func X \ Y -> Subset of X;

coherence

X \ Y is Subset of X

end;
:: original: \

redefine func X \ Y -> Subset of X;

coherence

X \ Y is Subset of X

proof end;

definition

let E be set ;

let A be Subset of E;

let X be set ;

:: original: \

redefine func A \ X -> Subset of E;

coherence

A \ X is Subset of E

end;
let A be Subset of E;

let X be set ;

:: original: \

redefine func A \ X -> Subset of E;

coherence

A \ X is Subset of E

proof end;

definition

let E be set ;

let A be Subset of E;

let X be set ;

:: original: /\

redefine func A /\ X -> Subset of E;

coherence

A /\ X is Subset of E

end;
let A be Subset of E;

let X be set ;

:: original: /\

redefine func A /\ X -> Subset of E;

coherence

A /\ X is Subset of E

proof end;

definition

let E, X be set ;

let A be Subset of E;

:: original: /\

redefine func X /\ A -> Subset of E;

coherence

X /\ A is Subset of E

end;
let A be Subset of E;

:: original: /\

redefine func X /\ A -> Subset of E;

coherence

X /\ A is Subset of E

proof end;

theorem :: SUBSET_1:11

canceled;

theorem :: SUBSET_1:12

canceled;

theorem :: SUBSET_1:13

canceled;

theorem :: SUBSET_1:14

canceled;

theorem :: SUBSET_1:15

for E being set

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B or x in C ) ) ) holds

A = B \/ C

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B or x in C ) ) ) holds

A = B \/ C

proof end;

theorem :: SUBSET_1:16

for E being set

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B & x in C ) ) ) holds

A = B /\ C

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B & x in C ) ) ) holds

A = B /\ C

proof end;

theorem :: SUBSET_1:17

for E being set

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B & not x in C ) ) ) holds

A = B \ C

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( x in B & not x in C ) ) ) holds

A = B \ C

proof end;

theorem :: SUBSET_1:18

for E being set

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds

A = B \+\ C

for A, B, C being Subset of E st ( for x being Element of E holds

( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds

A = B \+\ C

proof end;

theorem :: SUBSET_1:19

canceled;

theorem :: SUBSET_1:20

canceled;

theorem :: SUBSET_1:21

canceled;

theorem :: SUBSET_1:22

theorem :: SUBSET_1:23

canceled;

theorem :: SUBSET_1:24

canceled;

theorem Th25: :: SUBSET_1:25

proof end;

theorem :: SUBSET_1:26

canceled;

theorem :: SUBSET_1:27

canceled;

theorem :: SUBSET_1:28

proof end;

theorem :: SUBSET_1:29

canceled;

theorem :: SUBSET_1:30

canceled;

theorem Th31: :: SUBSET_1:31

proof end;

theorem :: SUBSET_1:32

proof end;

theorem :: SUBSET_1:33

proof end;

theorem :: SUBSET_1:34

proof end;

theorem :: SUBSET_1:35

proof end;

theorem :: SUBSET_1:36

proof end;

theorem :: SUBSET_1:37

canceled;

theorem :: SUBSET_1:38

proof end;

theorem :: SUBSET_1:39

proof end;

theorem :: SUBSET_1:40

for E, X being set

for A being Subset of E st X c= A & X c= A ` holds

X = {} by XBOOLE_1:67, XBOOLE_1:79;

for A being Subset of E st X c= A & X c= A ` holds

X = {} by XBOOLE_1:67, XBOOLE_1:79;

theorem :: SUBSET_1:41

proof end;

theorem :: SUBSET_1:42

proof end;

theorem Th43: :: SUBSET_1:43

proof end;

theorem :: SUBSET_1:44

proof end;

theorem :: SUBSET_1:45

canceled;

theorem :: SUBSET_1:46

proof end;

theorem :: SUBSET_1:47

proof end;

theorem :: SUBSET_1:48

for E being set

for A, B being Subset of E st ( for a being Element of A holds a in B ) holds

A c= B

for A, B being Subset of E st ( for a being Element of A holds a in B ) holds

A c= B

proof end;

theorem :: SUBSET_1:49

proof end;

theorem :: SUBSET_1:50

for E being set st E <> {} holds

for B being Subset of E

for x being Element of E st not x in B holds

x in B `

for B being Subset of E

for x being Element of E st not x in B holds

x in B `

proof end;

theorem Th51: :: SUBSET_1:51

for E being set

for A, B being Subset of E st ( for x being Element of E holds

( x in A iff not x in B ) ) holds

A = B `

for A, B being Subset of E st ( for x being Element of E holds

( x in A iff not x in B ) ) holds

A = B `

proof end;

theorem :: SUBSET_1:52

for E being set

for A, B being Subset of E st ( for x being Element of E holds

( not x in A iff x in B ) ) holds

A = B `

for A, B being Subset of E st ( for x being Element of E holds

( not x in A iff x in B ) ) holds

A = B `

proof end;

theorem :: SUBSET_1:53

for E being set

for A, B being Subset of E st ( for x being Element of E holds

( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds

A = B `

for A, B being Subset of E st ( for x being Element of E holds

( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds

A = B `

proof end;

theorem :: SUBSET_1:54

canceled;

theorem :: SUBSET_1:55

proof end;

theorem :: SUBSET_1:56

proof end;

theorem :: SUBSET_1:57

proof end;

theorem :: SUBSET_1:58

proof end;

theorem :: SUBSET_1:59

for X being set

for x1, x2, x3, x4, x5 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5} is Subset of X

for x1, x2, x3, x4, x5 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5} is Subset of X

proof end;

theorem :: SUBSET_1:60

for X being set

for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6} is Subset of X

for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6} is Subset of X

proof end;

theorem :: SUBSET_1:61

for X being set

for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6,x7} is Subset of X

for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6,x7} is Subset of X

proof end;

theorem :: SUBSET_1:62

for X being set

for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X

for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds

{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X

proof end;

theorem :: SUBSET_1:63

proof end;

scheme :: SUBSET_1:sch 2

SubsetEq{ F_{1}() -> set , F_{2}() -> Subset of F_{1}(), F_{3}() -> Subset of F_{1}(), P_{1}[ set ] } :

provided

SubsetEq{ F

provided

A1:
for y being Element of F_{1}() holds

( y in F_{2}() iff P_{1}[y] )
and

A2: for y being Element of F_{1}() holds

( y in F_{3}() iff P_{1}[y] )

( y in F

A2: for y being Element of F

( y in F

proof end;

definition

let X, Y be non empty set ;

:: original: misses

redefine pred X misses Y;

irreflexivity

for X being non empty set holds not X misses X

end;
:: original: misses

redefine pred X misses Y;

irreflexivity

for X being non empty set holds not X misses X

proof end;

definition

let X, Y be non empty set ;

:: original: misses

redefine pred X meets Y;

reflexivity

for X being non empty set holds not X misses X

end;
:: original: misses

redefine pred X meets Y;

reflexivity

for X being non empty set holds not X misses X

proof end;

definition

let S be set ;

func choose S -> Element of S equals :: SUBSET_1:def 6

the Element of S;

correctness

coherence

the Element of S is Element of S;

;

end;
func choose S -> Element of S equals :: SUBSET_1:def 6

the Element of S;

correctness

coherence

the Element of S is Element of S;

;

:: deftheorem defines choose SUBSET_1:def 6 :

for S being set holds choose S = the Element of S;

begin

Lm2: for X, Y being set st ( for x being set st x in X holds

x in Y ) holds

X is Subset of Y

proof end;

Lm3: for x, E being set

for A being Subset of E st x in A holds

x is Element of E

proof end;

scheme :: SUBSET_1:sch 4

SubComp{ F_{1}() -> set , F_{2}() -> Subset of F_{1}(), F_{3}() -> Subset of F_{1}(), P_{1}[ set ] } :

provided

SubComp{ F

provided

A1:
for X being Element of F_{1}() holds

( X in F_{2}() iff P_{1}[X] )
and

A2: for X being Element of F_{1}() holds

( X in F_{3}() iff P_{1}[X] )

( X in F

A2: for X being Element of F

( X in F

proof end;

theorem :: SUBSET_1:64

proof end;

registration

let X be empty set ;

cluster -> empty Element of bool X;

coherence

for b_{1} being Subset of X holds b_{1} is empty

end;
cluster -> empty Element of bool X;

coherence

for b

proof end;

:: deftheorem defines proper SUBSET_1:def 7 :

for E being set

for A being Subset of E holds

( A is proper iff A <> E );

registration
end;

registration

let E be set ;

cluster non proper Element of bool E;

existence

not for b_{1} being Subset of E holds b_{1} is proper

end;
cluster non proper Element of bool E;

existence

not for b

proof end;

registration

let E be non empty set ;

cluster non proper -> non empty Element of bool E;

coherence

for b_{1} being Subset of E st not b_{1} is proper holds

not b_{1} is empty

coherence

for b_{1} being Subset of E st b_{1} is empty holds

b_{1} is proper
;

end;
cluster non proper -> non empty Element of bool E;

coherence

for b

not b

proof end;

cluster empty -> proper Element of bool E;coherence

for b

b

registration

let E be non empty set ;

cluster proper Element of bool E;

existence

ex b_{1} being Subset of E st b_{1} is proper

end;
cluster proper Element of bool E;

existence

ex b

proof end;

registration

let E be empty set ;

cluster -> non proper Element of bool E;

coherence

for b_{1} being Subset of E holds not b_{1} is proper

end;
cluster -> non proper Element of bool E;

coherence

for b

proof end;

theorem :: SUBSET_1:65

for X, Y, A, z being set st z in A & A c= [:X,Y:] holds

ex x being Element of X ex y being Element of Y st z = [x,y]

ex x being Element of X ex y being Element of Y st z = [x,y]

proof end;