:: Boolean Properties of Sets - Theorems
:: by Library Committee
::
:: Received April 08, 2002
:: Copyright (c) 2002 Association of Mizar Users

begin

theorem Th1: :: XBOOLE_1:1

for X, Y, Z being set st X c= Y & Y c= Z holds
X c= Z

proof end;

theorem Th2: :: XBOOLE_1:2

for X being set holds {} c= X

proof end;

theorem Th3: :: XBOOLE_1:3

for X being set st X c= {} holds
X = {}

proof end;

theorem Th4: :: XBOOLE_1:4

for X, Y, Z being set holds (X \/ Y) \/ Z = X \/ (Y \/ Z)

proof end;

theorem :: XBOOLE_1:5

for X, Y, Z being set holds (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)

proof end;

theorem :: XBOOLE_1:6

for X, Y being set holds X \/ (X \/ Y) = X \/ Y

proof end;

theorem Th7: :: XBOOLE_1:7

for X, Y being set holds X c= X \/ Y

proof end;

theorem Th8: :: XBOOLE_1:8

for X, Z, Y being set st X c= Z & Y c= Z holds
X \/ Y c= Z

proof end;

theorem :: XBOOLE_1:9

for X, Y, Z being set st X c= Y holds
X \/ Z c= Y \/ Z

proof end;

theorem :: XBOOLE_1:10

for X, Y, Z being set st X c= Y holds
X c= Z \/ Y

proof end;

theorem :: XBOOLE_1:11

for X, Y, Z being set st X \/ Y c= Z holds
X c= Z

proof end;

theorem Th12: :: XBOOLE_1:12

for X, Y being set st X c= Y holds
X \/ Y = Y

proof end;

theorem :: XBOOLE_1:13

for X, Y, Z, V being set st X c= Y & Z c= V holds
X \/ Z c= Y \/ V

proof end;

theorem :: XBOOLE_1:14

for Y, X, Z being set st Y c= X & Z c= X & ( for V being set st Y c= V & Z c= V holds
X c= V ) holds
X = Y \/ Z

proof end;

theorem :: XBOOLE_1:15

for X, Y being set st X \/ Y = {} holds
X = {} ;

theorem Th16: :: XBOOLE_1:16

for X, Y, Z being set holds (X /\ Y) /\ Z = X /\ (Y /\ Z)

proof end;

theorem Th17: :: XBOOLE_1:17

for X, Y being set holds X /\ Y c= X

proof end;

theorem :: XBOOLE_1:18

for X, Y, Z being set st X c= Y /\ Z holds
X c= Y

proof end;

theorem Th19: :: XBOOLE_1:19

for Z, X, Y being set st Z c= X & Z c= Y holds
Z c= X /\ Y

proof end;

theorem :: XBOOLE_1:20

for X, Y, Z being set st X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds
V c= X ) holds
X = Y /\ Z

proof end;

theorem :: XBOOLE_1:21

for X, Y being set holds X /\ (X \/ Y) = X

proof end;

theorem Th22: :: XBOOLE_1:22

for X, Y being set holds X \/ (X /\ Y) = X

proof end;

theorem Th23: :: XBOOLE_1:23

for X, Y, Z being set holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)

proof end;

theorem Th24: :: XBOOLE_1:24

for X, Y, Z being set holds X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)

proof end;

theorem :: XBOOLE_1:25

for X, Y, Z being set holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)

proof end;

theorem Th26: :: XBOOLE_1:26

for X, Y, Z being set st X c= Y holds
X /\ Z c= Y /\ Z

proof end;

theorem :: XBOOLE_1:27

for X, Y, Z, V being set st X c= Y & Z c= V holds
X /\ Z c= Y /\ V

proof end;

theorem Th28: :: XBOOLE_1:28

for X, Y being set st X c= Y holds
X /\ Y = X

proof end;

theorem :: XBOOLE_1:29

for X, Y, Z being set holds X /\ Y c= X \/ Z

proof end;

theorem :: XBOOLE_1:30

for X, Z, Y being set st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z

proof end;

theorem :: XBOOLE_1:31

for X, Y, Z being set holds (X /\ Y) \/ (X /\ Z) c= Y \/ Z

proof end;

Lm1: for X, Y being set holds
( X \ Y = {} iff X c= Y )

proof end;

theorem :: XBOOLE_1:32

for X, Y being set st X \ Y = Y \ X holds
X = Y

proof end;

theorem Th33: :: XBOOLE_1:33

for X, Y, Z being set st X c= Y holds
X \ Z c= Y \ Z

proof end;

theorem Th34: :: XBOOLE_1:34

for X, Y, Z being set st X c= Y holds
Z \ Y c= Z \ X

proof end;

Lm2: for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)

proof end;

theorem :: XBOOLE_1:35

for X, Y, Z, V being set st X c= Y & Z c= V holds
X \ V c= Y \ Z

proof end;

theorem Th36: :: XBOOLE_1:36

for X, Y being set holds X \ Y c= X

proof end;

theorem :: XBOOLE_1:37

for X, Y being set holds
( X \ Y = {} iff X c= Y ) by Lm1;

theorem :: XBOOLE_1:38

for X, Y being set st X c= Y \ X holds
X = {}

proof end;

theorem Th39: :: XBOOLE_1:39

for X, Y being set holds X \/ (Y \ X) = X \/ Y

proof end;

theorem :: XBOOLE_1:40

for X, Y being set holds (X \/ Y) \ Y = X \ Y

proof end;

theorem Th41: :: XBOOLE_1:41

for X, Y, Z being set holds (X \ Y) \ Z = X \ (Y \/ Z)

proof end;

theorem Th42: :: XBOOLE_1:42

for X, Y, Z being set holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)

proof end;

theorem :: XBOOLE_1:43

for X, Y, Z being set st X c= Y \/ Z holds
X \ Y c= Z

proof end;

theorem :: XBOOLE_1:44

for X, Y, Z being set st X \ Y c= Z holds
X c= Y \/ Z

proof end;

theorem :: XBOOLE_1:45

for X, Y being set st X c= Y holds
Y = X \/ (Y \ X)

proof end;

theorem :: XBOOLE_1:46

for X, Y being set holds X \ (X \/ Y) = {}

proof end;

theorem Th47: :: XBOOLE_1:47

for X, Y being set holds X \ (X /\ Y) = X \ Y

proof end;

theorem :: XBOOLE_1:48

for X, Y being set holds X \ (X \ Y) = X /\ Y

proof end;

theorem Th49: :: XBOOLE_1:49

for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ Z

proof end;

theorem Th50: :: XBOOLE_1:50

for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)

proof end;

theorem Th51: :: XBOOLE_1:51

for X, Y being set holds (X /\ Y) \/ (X \ Y) = X

proof end;

theorem Th52: :: XBOOLE_1:52

for X, Y, Z being set holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)

proof end;

theorem :: XBOOLE_1:53

for X, Y, Z being set holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)

proof end;

theorem :: XBOOLE_1:54

for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z) by Lm2;

theorem Th55: :: XBOOLE_1:55

for X, Y being set holds (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)

proof end;

Lm3: for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z

proof end;

theorem :: XBOOLE_1:56

for X, Y, Z being set st X c< Y & Y c< Z holds
X c< Z

proof end;

theorem :: XBOOLE_1:57

for X, Y being set holds
( not X c< Y or not Y c< X ) ;

theorem :: XBOOLE_1:58

for X, Y, Z being set st X c< Y & Y c= Z holds
X c< Z

proof end;

theorem :: XBOOLE_1:59

for X, Y, Z being set st X c= Y & Y c< Z holds
X c< Z by Lm3;

theorem Th60: :: XBOOLE_1:60

for X, Y being set st X c= Y holds
not Y c< X

proof end;

theorem :: XBOOLE_1:61

for X being set st X <> {} holds
{} c< X

proof end;

theorem :: XBOOLE_1:62

for X being set holds not X c< {}

proof end;

theorem Th63: :: XBOOLE_1:63

for X, Y, Z being set st X c= Y & Y misses Z holds
X misses Z

proof end;

theorem :: XBOOLE_1:64

for A, X, B, Y being set st A c= X & B c= Y & X misses Y holds
A misses B

proof end;

theorem :: XBOOLE_1:65

for X being set holds X misses {}

proof end;

theorem :: XBOOLE_1:66

for X being set holds
( X meets X iff X <> {} )

proof end;

theorem :: XBOOLE_1:67

for X, Y, Z being set st X c= Y & X c= Z & Y misses Z holds
X = {}

proof end;

theorem :: XBOOLE_1:68

for Y, Z being set
for A being non empty set st A c= Y & A c= Z holds
Y meets Z

proof end;

theorem :: XBOOLE_1:69

for Y being set
for A being non empty set st A c= Y holds
A meets Y

proof end;

theorem Th70: :: XBOOLE_1:70

for X, Y, Z being set holds
( ( X meets Y or X meets Z ) iff X meets Y \/ Z )

proof end;

theorem :: XBOOLE_1:71

for X, Y, Z being set st X \/ Y = Z \/ Y & X misses Y & Z misses Y holds
X = Z

proof end;

theorem :: XBOOLE_1:72

for X9, Y9, X, Y being set st X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 holds
X = Y9

proof end;

theorem :: XBOOLE_1:73

for X, Y, Z being set st X c= Y \/ Z & X misses Z holds
X c= Y

proof end;

theorem Th74: :: XBOOLE_1:74

for X, Y, Z being set st X meets Y /\ Z holds
X meets Y

proof end;

theorem :: XBOOLE_1:75

for X, Y being set st X meets Y holds
X /\ Y meets Y

proof end;

theorem :: XBOOLE_1:76

for Y, Z, X being set st Y misses Z holds
X /\ Y misses X /\ Z

proof end;

theorem :: XBOOLE_1:77

for X, Y, Z being set st X meets Y & X c= Z holds
X meets Y /\ Z

proof end;

theorem :: XBOOLE_1:78

for X, Y, Z being set st X misses Y holds
X /\ (Y \/ Z) = X /\ Z

proof end;

theorem Th79: :: XBOOLE_1:79

for X, Y being set holds X \ Y misses Y

proof end;

theorem :: XBOOLE_1:80

for X, Y, Z being set st X misses Y holds
X misses Y \ Z

proof end;

theorem :: XBOOLE_1:81

for X, Y, Z being set st X misses Y \ Z holds
Y misses X \ Z

proof end;

theorem :: XBOOLE_1:82

for X, Y being set holds X \ Y misses Y \ X

proof end;

theorem Th83: :: XBOOLE_1:83

for X, Y being set holds
( X misses Y iff X \ Y = X )

proof end;

theorem :: XBOOLE_1:84

for X, Y, Z being set st X meets Y & X misses Z holds
X meets Y \ Z

proof end;

theorem :: XBOOLE_1:85

for X, Y, Z being set st X c= Y holds
X misses Z \ Y

proof end;

theorem Th86: :: XBOOLE_1:86

for X, Y, Z being set st X c= Y & X misses Z holds
X c= Y \ Z

proof end;

theorem :: XBOOLE_1:87

for Y, Z, X being set st Y misses Z holds
(X \ Y) \/ Z = (X \/ Z) \ Y

proof end;

theorem Th88: :: XBOOLE_1:88

for X, Y being set st X misses Y holds
(X \/ Y) \ Y = X

proof end;

theorem Th89: :: XBOOLE_1:89

for X, Y being set holds X /\ Y misses X \ Y

proof end;

theorem :: XBOOLE_1:90

for X, Y being set holds X \ (X /\ Y) misses Y

proof end;

theorem :: XBOOLE_1:91

for X, Y, Z being set holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)

proof end;

theorem :: XBOOLE_1:92

for X being set holds X \+\ X = {} by Lm1;

theorem Th93: :: XBOOLE_1:93

for X, Y being set holds X \/ Y = (X \+\ Y) \/ (X /\ Y)

proof end;

Lm4: for X, Y being set holds X /\ Y misses X \+\ Y

proof end;

Lm5: for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y)

proof end;

theorem :: XBOOLE_1:94

for X, Y being set holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)

proof end;

theorem :: XBOOLE_1:95

for X, Y being set holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)

proof end;

theorem :: XBOOLE_1:96

for X, Y being set holds X \ Y c= X \+\ Y by Th7;

theorem :: XBOOLE_1:97

for X, Y, Z being set st X \ Y c= Z & Y \ X c= Z holds
X \+\ Y c= Z by Th8;

theorem :: XBOOLE_1:98

for X, Y being set holds X \/ Y = X \+\ (Y \ X)

proof end;

theorem :: XBOOLE_1:99

for X, Y, Z being set holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))

proof end;

theorem :: XBOOLE_1:100

for X, Y being set holds X \ Y = X \+\ (X /\ Y)

proof end;

theorem :: XBOOLE_1:101

for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y) by Lm5;

theorem :: XBOOLE_1:102

for X, Y, Z being set holds X \ (Y \+\ Z) = (X \ (Y \/ Z)) \/ ((X /\ Y) /\ Z)

proof end;

theorem :: XBOOLE_1:103

for X, Y being set holds X /\ Y misses X \+\ Y by Lm4;

theorem :: XBOOLE_1:104

for X, Y being set holds
( ( X c< Y or X = Y or Y c< X ) iff X,Y are_c=-comparable )

proof end;

begin

theorem :: XBOOLE_1:105

for X, Y being set st X c< Y holds
Y \ X <> {}

proof end;

theorem Th106: :: XBOOLE_1:106

for X, A, B being set st X c= A \ B holds
( X c= A & X misses B )

proof end;

theorem :: XBOOLE_1:107

for X, A, B being set holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )

proof end;

theorem :: XBOOLE_1:108

for X, A, Y being set st X c= A holds
X /\ Y c= A

proof end;

theorem Th109: :: XBOOLE_1:109

for X, A, Y being set st X c= A holds
X \ Y c= A

proof end;

theorem :: XBOOLE_1:110

for X, A, Y being set st X c= A & Y c= A holds
X \+\ Y c= A

proof end;

theorem Th111: :: XBOOLE_1:111

for X, Z, Y being set holds (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z

proof end;

theorem :: XBOOLE_1:112

for X, Z, Y being set holds (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z

proof end;

theorem :: XBOOLE_1:113

for X, Y, Z, V being set holds ((X \/ Y) \/ Z) \/ V = X \/ ((Y \/ Z) \/ V)

proof end;

theorem :: XBOOLE_1:114

for A, B, C, D being set st A misses D & B misses D & C misses D holds
(A \/ B) \/ C misses D

proof end;

theorem :: XBOOLE_1:115

for A being set holds not A c< {}

proof end;

theorem :: XBOOLE_1:116

for X, Y, Z being set holds X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)

proof end;

theorem :: XBOOLE_1:117

for P, G, C being set st C c= G holds
P \ C = (P \ G) \/ (P /\ (G \ C))

proof end;