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

:: WP: Modus Celarent
:: WP: Modus Darii
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;

:: WP: Modus Darapti
theorem Th68: :: 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 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 )
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;