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


begin

:: [WP: ] Modus_Barbara
theorem Th1: :: XBOOLE_1:1
for X, Y, Z being set st X c= Y & Y c= Z holds
X c= Z
proofend;

theorem Th2: :: XBOOLE_1:2
for X being set holds {} c= X
proofend;

theorem Th3: :: XBOOLE_1:3
for X being set st X c= {} holds
X = {}
proofend;

theorem Th4: :: XBOOLE_1:4
for X, Y, Z being set holds (X \/ Y) \/ Z = X \/ (Y \/ Z)
proofend;

theorem :: XBOOLE_1:5
for X, Y, Z being set holds (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
proofend;

theorem :: XBOOLE_1:6
for X, Y being set holds X \/ (X \/ Y) = X \/ Y
proofend;

theorem Th7: :: XBOOLE_1:7
for X, Y being set holds X c= X \/ Y
proofend;

theorem Th8: :: XBOOLE_1:8
for X, Z, Y being set st X c= Z & Y c= Z holds
X \/ Y c= Z
proofend;

theorem :: XBOOLE_1:9
for X, Y, Z being set st X c= Y holds
X \/ Z c= Y \/ Z
proofend;

theorem :: XBOOLE_1:10
for X, Y, Z being set st X c= Y holds
X c= Z \/ Y
proofend;

theorem :: XBOOLE_1:11
for X, Y, Z being set st X \/ Y c= Z holds
X c= Z
proofend;

theorem Th12: :: XBOOLE_1:12
for X, Y being set st X c= Y holds
X \/ Y = Y
proofend;

theorem :: XBOOLE_1:13
for X, Y, Z, V being set st X c= Y & Z c= V holds
X \/ Z c= Y \/ V
proofend;

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

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)
proofend;

theorem Th17: :: XBOOLE_1:17
for X, Y being set holds X /\ Y c= X
proofend;

theorem :: XBOOLE_1:18
for X, Y, Z being set st X c= Y /\ Z holds
X c= Y
proofend;

theorem Th19: :: XBOOLE_1:19
for Z, X, Y being set st Z c= X & Z c= Y holds
Z c= X /\ Y
proofend;

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

theorem :: XBOOLE_1:21
for X, Y being set holds X /\ (X \/ Y) = X
proofend;

theorem Th22: :: XBOOLE_1:22
for X, Y being set holds X \/ (X /\ Y) = X
proofend;

theorem Th23: :: XBOOLE_1:23
for X, Y, Z being set holds X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z)
proofend;

theorem Th24: :: XBOOLE_1:24
for X, Y, Z being set holds X \/ (Y /\ Z) = (X \/ Y) /\ (X \/ Z)
proofend;

theorem :: XBOOLE_1:25
for X, Y, Z being set holds ((X /\ Y) \/ (Y /\ Z)) \/ (Z /\ X) = ((X \/ Y) /\ (Y \/ Z)) /\ (Z \/ X)
proofend;

theorem Th26: :: XBOOLE_1:26
for X, Y, Z being set st X c= Y holds
X /\ Z c= Y /\ Z
proofend;

theorem :: XBOOLE_1:27
for X, Y, Z, V being set st X c= Y & Z c= V holds
X /\ Z c= Y /\ V
proofend;

theorem Th28: :: XBOOLE_1:28
for X, Y being set st X c= Y holds
X /\ Y = X
proofend;

theorem :: XBOOLE_1:29
for X, Y, Z being set holds X /\ Y c= X \/ Z
proofend;

theorem :: XBOOLE_1:30
for X, Z, Y being set st X c= Z holds
X \/ (Y /\ Z) = (X \/ Y) /\ Z
proofend;

theorem :: XBOOLE_1:31
for X, Y, Z being set holds (X /\ Y) \/ (X /\ Z) c= Y \/ Z
proofend;

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

theorem :: XBOOLE_1:32
for X, Y being set st X \ Y = Y \ X holds
X = Y
proofend;

theorem Th33: :: XBOOLE_1:33
for X, Y, Z being set st X c= Y holds
X \ Z c= Y \ Z
proofend;

theorem Th34: :: XBOOLE_1:34
for X, Y, Z being set st X c= Y holds
Z \ Y c= Z \ X
proofend;

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

theorem :: XBOOLE_1:35
for X, Y, Z, V being set st X c= Y & Z c= V holds
X \ V c= Y \ Z
proofend;

theorem Th36: :: XBOOLE_1:36
for X, Y being set holds X \ Y c= X
proofend;

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 = {}
proofend;

theorem Th39: :: XBOOLE_1:39
for X, Y being set holds X \/ (Y \ X) = X \/ Y
proofend;

theorem :: XBOOLE_1:40
for X, Y being set holds (X \/ Y) \ Y = X \ Y
proofend;

theorem Th41: :: XBOOLE_1:41
for X, Y, Z being set holds (X \ Y) \ Z = X \ (Y \/ Z)
proofend;

theorem Th42: :: XBOOLE_1:42
for X, Y, Z being set holds (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z)
proofend;

theorem :: XBOOLE_1:43
for X, Y, Z being set st X c= Y \/ Z holds
X \ Y c= Z
proofend;

theorem :: XBOOLE_1:44
for X, Y, Z being set st X \ Y c= Z holds
X c= Y \/ Z
proofend;

theorem :: XBOOLE_1:45
for X, Y being set st X c= Y holds
Y = X \/ (Y \ X)
proofend;

theorem :: XBOOLE_1:46
for X, Y being set holds X \ (X \/ Y) = {}
proofend;

theorem Th47: :: XBOOLE_1:47
for X, Y being set holds X \ (X /\ Y) = X \ Y
proofend;

theorem :: XBOOLE_1:48
for X, Y being set holds X \ (X \ Y) = X /\ Y
proofend;

theorem Th49: :: XBOOLE_1:49
for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ Z
proofend;

theorem Th50: :: XBOOLE_1:50
for X, Y, Z being set holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
proofend;

theorem Th51: :: XBOOLE_1:51
for X, Y being set holds (X /\ Y) \/ (X \ Y) = X
proofend;

theorem Th52: :: XBOOLE_1:52
for X, Y, Z being set holds X \ (Y \ Z) = (X \ Y) \/ (X /\ Z)
proofend;

theorem :: XBOOLE_1:53
for X, Y, Z being set holds X \ (Y \/ Z) = (X \ Y) /\ (X \ Z)
proofend;

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)
proofend;

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

theorem :: XBOOLE_1:56
for X, Y, Z being set st X c< Y &amp; Y c< Z holds
X c< Z
proofend;

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 &amp; Y c= Z holds
X c< Z
proofend;

theorem :: XBOOLE_1:59
for X, Y, Z being set st X c= Y &amp; 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
proofend;

theorem :: XBOOLE_1:61
for X being set st X <> {} holds
{} c< X
proofend;

theorem :: XBOOLE_1:62
for X being set holds not X c< {}
proofend;

:: [WP: ] Modus_Celarent
:: [WP: ] Modus_Darii
theorem Th63: :: XBOOLE_1:63
for X, Y, Z being set st X c= Y &amp; Y misses Z holds
X misses Z
proofend;

theorem :: XBOOLE_1:64
for A, X, B, Y being set st A c= X &amp; B c= Y &amp; X misses Y holds
A misses B
proofend;

theorem :: XBOOLE_1:65
for X being set holds X misses {}
proofend;

theorem :: XBOOLE_1:66
for X being set holds
( X meets X iff X <> {} )
proofend;

theorem :: XBOOLE_1:67
for X, Y, Z being set st X c= Y &amp; X c= Z &amp; Y misses Z holds
X = {}
proofend;

:: [WP: ] Modus_Darapti
theorem Th68: :: XBOOLE_1:68
for Y, Z being set
for A being non empty set st A c= Y &amp; A c= Z holds
Y meets Z
proofend;

theorem :: XBOOLE_1:69
for Y being set
for A being non empty set st A c= Y holds
A meets Y by Th68;

theorem Th70: :: XBOOLE_1:70
for X, Y, Z being set holds
( ( X meets Y or X meets Z ) iff X meets Y \/ Z )
proofend;

theorem :: XBOOLE_1:71
for X, Y, Z being set st X \/ Y = Z \/ Y &amp; X misses Y &amp; Z misses Y holds
X = Z
proofend;

theorem :: XBOOLE_1:72
for X9, Y9, X, Y being set st X9 \/ Y9 = X \/ Y &amp; X misses X9 &amp; Y misses Y9 holds
X = Y9
proofend;

theorem :: XBOOLE_1:73
for X, Y, Z being set st X c= Y \/ Z &amp; X misses Z holds
X c= Y
proofend;

theorem Th74: :: XBOOLE_1:74
for X, Y, Z being set st X meets Y /\ Z holds
X meets Y
proofend;

theorem :: XBOOLE_1:75
for X, Y being set st X meets Y holds
X /\ Y meets Y
proofend;

theorem :: XBOOLE_1:76
for Y, Z, X being set st Y misses Z holds
X /\ Y misses X /\ Z
proofend;

theorem :: XBOOLE_1:77
for X, Y, Z being set st X meets Y &amp; X c= Z holds
X meets Y /\ Z
proofend;

theorem :: XBOOLE_1:78
for X, Y, Z being set st X misses Y holds
X /\ (Y \/ Z) = X /\ Z
proofend;

theorem Th79: :: XBOOLE_1:79
for X, Y being set holds X \ Y misses Y
proofend;

theorem :: XBOOLE_1:80
for X, Y, Z being set st X misses Y holds
X misses Y \ Z
proofend;

theorem :: XBOOLE_1:81
for X, Y, Z being set st X misses Y \ Z holds
Y misses X \ Z
proofend;

theorem :: XBOOLE_1:82
for X, Y being set holds X \ Y misses Y \ X
proofend;

theorem Th83: :: XBOOLE_1:83
for X, Y being set holds
( X misses Y iff X \ Y = X )
proofend;

theorem :: XBOOLE_1:84
for X, Y, Z being set st X meets Y &amp; X misses Z holds
X meets Y \ Z
proofend;

theorem :: XBOOLE_1:85
for X, Y, Z being set st X c= Y holds
X misses Z \ Y
proofend;

theorem Th86: :: XBOOLE_1:86
for X, Y, Z being set st X c= Y &amp; X misses Z holds
X c= Y \ Z
proofend;

theorem :: XBOOLE_1:87
for Y, Z, X being set st Y misses Z holds
(X \ Y) \/ Z = (X \/ Z) \ Y
proofend;

theorem Th88: :: XBOOLE_1:88
for X, Y being set st X misses Y holds
(X \/ Y) \ Y = X
proofend;

theorem Th89: :: XBOOLE_1:89
for X, Y being set holds X /\ Y misses X \ Y
proofend;

theorem :: XBOOLE_1:90
for X, Y being set holds X \ (X /\ Y) misses Y
proofend;

theorem :: XBOOLE_1:91
for X, Y, Z being set holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proofend;

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)
proofend;

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

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

theorem :: XBOOLE_1:94
for X, Y being set holds X \/ Y = (X \+\ Y) \+\ (X /\ Y)
proofend;

theorem :: XBOOLE_1:95
for X, Y being set holds X /\ Y = (X \+\ Y) \+\ (X \/ Y)
proofend;

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 &amp; 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)
proofend;

theorem :: XBOOLE_1:99
for X, Y, Z being set holds (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z))
proofend;

theorem :: XBOOLE_1:100
for X, Y being set holds X \ Y = X \+\ (X /\ Y)
proofend;

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)
proofend;

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 )
proofend;

begin

theorem :: XBOOLE_1:105
for X, Y being set st X c< Y holds
Y \ X <> {}
proofend;

theorem Th106: :: XBOOLE_1:106
for X, A, B being set st X c= A \ B holds
( X c= A &amp; X misses B )
proofend;

theorem :: XBOOLE_1:107
for X, A, B being set holds
( X c= A \+\ B iff ( X c= A \/ B &amp; X misses A /\ B ) )
proofend;

theorem :: XBOOLE_1:108
for X, A, Y being set st X c= A holds
X /\ Y c= A
proofend;

theorem Th109: :: XBOOLE_1:109
for X, A, Y being set st X c= A holds
X \ Y c= A
proofend;

theorem :: XBOOLE_1:110
for X, A, Y being set st X c= A &amp; Y c= A holds
X \+\ Y c= A
proofend;

theorem Th111: :: XBOOLE_1:111
for X, Z, Y being set holds (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z
proofend;

theorem :: XBOOLE_1:112
for X, Z, Y being set holds (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z
proofend;

theorem :: XBOOLE_1:113
for X, Y, Z, V being set holds ((X \/ Y) \/ Z) \/ V = X \/ ((Y \/ Z) \/ V)
proofend;

theorem :: XBOOLE_1:114
for A, B, C, D being set st A misses D &amp; B misses D &amp; C misses D holds
(A \/ B) \/ C misses D
proofend;

theorem :: XBOOLE_1:115
for A being set holds not A c< {}
proofend;

theorem :: XBOOLE_1:116
for X, Y, Z being set holds X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z)
proofend;

theorem :: XBOOLE_1:117
for P, G, C being set st C c= G holds
P \ C = (P \ G) \/ (P /\ (G \ C))
proofend;