B.5 XBOOLE_1

Boolean Properties of Sets --- Theorems by Library Committee

reserve x,A,B,X,X',Y,Y',Z,V for set;

1 X c= Y & Y c= Z implies X c= Z;
2 {} c= X;
3 X c= {} implies X = {};
4 (X \/ Y) \/ Z = X \/ (Y \/ Z);
5 (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z);
6 X \/ (X \/ Y) = X \/ Y;
7 X c= X \/ Y;
8 X c= Z & Y c= Z implies X \/ Y c= Z;
9 X c= Y implies X \/ Z c= Y \/ Z;
10 X c= Y implies X c= Z \/ Y;
11 X \/ Y c= Z implies X c= Z;
12 X c= Y implies X \/ Y = Y;
13 X c= Y & Z c= V implies X \/ Z c= Y \/ V;
14 (Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = Y \/ Z;
15 X \/ Y = {} implies X = {};
16 (X /\ Y) /\ Z = X /\ (Y /\ Z);
17 X /\ Y c= X;
18 X c= Y /\ Z implies X c= Y;
19 Z c= X & Z c= Y implies Z c= X /\ Y;
20 (X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = Y /\ Z;
21 X /\ (X \/ Y) = X;
22 X \/ (X /\ Y) = X;
23 X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;
24 X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);
25 (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);
26 X c= Y implies X /\ Z c= Y /\ Z;
27 X c= Y & Z c= V implies X /\ Z c= Y /\ V;
28 X c= Y implies X /\ Y = X;
29 X /\ Y c= X \/ Z;
30 X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;
31 (X /\ Y) \/ (X /\ Z) c= Y \/ Z;
32 X \ Y = Y \ X implies X = Y;
33 X c= Y implies X \ Z c= Y \ Z;
34 X c= Y implies Z \ Y c= Z \ X;
35 X c= Y & Z c= V implies X \ V c= Y \ Z;
36 X \ Y c= X;
37 X \ Y = {} iff X c= Y;
38 X c= Y \ X implies X = {};
39 X \/ (Y \ X) = X \/ Y;
40 (X \/ Y) \ Y = X \ Y;
41 (X \ Y) \ Z = X \ (Y \/ Z);
42 (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);
43 X c= Y \/ Z implies X \ Y c= Z;
44 X \ Y c= Z implies X c= Y \/ Z;
45 X c= Y implies Y = X \/ (Y \ X);
46 X \ (X \/ Y) = {};
47 X \ X /\ Y = X \ Y;
48 X \ (X \ Y) = X /\ Y;
49 X /\ (Y \ Z) = (X /\ Y) \ Z;
50 X /\ (Y \ Z) = X /\ Y \ X /\ Z;
51 X /\ Y \/ (X \ Y) = X;
52 X \ (Y \ Z) = (X \ Y) \/ X /\ Z;
53 X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);
54 X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);
55 (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);
56 X c< Y & Y c< Z implies X c< Z;
57 not (X c< Y & Y c< X);
58 X c< Y & Y c= Z implies X c< Z;
59 X c= Y & Y c< Z implies X c< Z;
60 X c= Y implies not Y c< X;
61 X <> {} implies {} c< X;
62 not X c< {};
63 X c= Y & Y misses Z implies X misses Z;
64 A c= X & B c= Y & X misses Y implies A misses B;
65 X misses {};
66 X meets X iff X <> {};
67 X c= Y & X c= Z & Y misses Z implies X = {};
68 for A being non empty set st A c= Y & A c= Z holds Y meets Z;
69 for A being non empty set st A c= Y holds A meets Y;
70 X meets Y \/ Z iff X meets Y or X meets Z;
71 X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z;
72 X' \/ Y' = X \/ Y & X misses X' & Y misses Y' implies X = Y';
73 X c= Y \/ Z & X misses Z implies X c= Y;
74 X meets Y /\ Z implies X meets Y;
75 X meets Y implies X /\ Y meets Y;
76 Y misses Z implies X /\ Y misses X /\ Z;
77 X meets Y & X c= Z implies X meets Y /\ Z;
78 X misses Y implies X /\ (Y \/ Z) = X /\ Z;
79 X \ Y misses Y;
80 X misses Y implies X misses Y \ Z;
81 X misses Y \ Z implies Y misses X \ Z;
82 X \ Y misses Y \ X;
83 X misses Y iff X \ Y = X;
84 X meets Y & X misses Z implies X meets Y \ Z;
85 X c= Y implies X misses Z \ Y;
86 X c= Y & X misses Z implies X c= Y \ Z;
87 Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y;
88 X misses Y implies (X \/ Y) \ Y = X;
89 X /\ Y misses X \ Y;
90 X \ (X /\ Y) misses Y;
91 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);
92 X \+\ X = {};
93 X \/ Y = (X \+\ Y) \/ X /\ Y;
94 X \/ Y = X \+\ Y \+\ X /\ Y;
95 X /\ Y = X \+\ Y \+\ (X \/ Y);
96 X \ Y c= X \+\ Y;
97 X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;
98 X \/ Y = X \+\ (Y \ X);
99 (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));
100 X \ Y = X \+\ (X /\ Y);
101 X \+\ Y = (X \/ Y) \ X /\ Y;
102 X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;
103 X /\ Y misses X \+\ Y;
104 X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable;