:: Boolean Properties of Sets - Theorems :: by Library Committee :: :: Received April 08, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TARSKI, XBOOLE_0; notations TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; registrations XBOOLE_0; requirements BOOLE; begin reserve x,A,B,X,X9,Y,Y9,Z,V for set; ::$N Modus Barbara theorem :: XBOOLE_1:1 X c= Y & Y c= Z implies X c= Z; theorem :: XBOOLE_1:2 {} c= X; theorem :: XBOOLE_1:3 X c= {} implies X = {}; theorem :: XBOOLE_1:4 (X \/ Y) \/ Z = X \/ (Y \/ Z); theorem :: XBOOLE_1:5 (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z); theorem :: XBOOLE_1:6 X \/ (X \/ Y) = X \/ Y; theorem :: XBOOLE_1:7 X c= X \/ Y; theorem :: XBOOLE_1:8 X c= Z & Y c= Z implies X \/ Y c= Z; theorem :: XBOOLE_1:9 X c= Y implies X \/ Z c= Y \/ Z; theorem :: XBOOLE_1:10 X c= Y implies X c= Z \/ Y; theorem :: XBOOLE_1:11 X \/ Y c= Z implies X c= Z; theorem :: XBOOLE_1:12 X c= Y implies X \/ Y = Y; theorem :: XBOOLE_1:13 X c= Y & Z c= V implies X \/ Z c= Y \/ V; theorem :: XBOOLE_1:14 (Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V) implies X = Y \/ Z; theorem :: XBOOLE_1:15 X \/ Y = {} implies X = {}; theorem :: XBOOLE_1:16 (X /\ Y) /\ Z = X /\ (Y /\ Z); theorem :: XBOOLE_1:17 X /\ Y c= X; theorem :: XBOOLE_1:18 X c= Y /\ Z implies X c= Y; theorem :: XBOOLE_1:19 Z c= X & Z c= Y implies Z c= X /\ Y; theorem :: XBOOLE_1:20 (X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X) implies X = Y /\ Z; theorem :: XBOOLE_1:21 X /\ (X \/ Y) = X; theorem :: XBOOLE_1:22 X \/ (X /\ Y) = X; theorem :: XBOOLE_1:23 X /\ (Y \/ Z) = X /\ Y \/ X /\ Z; theorem :: XBOOLE_1:24 X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z); theorem :: XBOOLE_1:25 (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X); theorem :: XBOOLE_1:26 X c= Y implies X /\ Z c= Y /\ Z; theorem :: XBOOLE_1:27 X c= Y & Z c= V implies X /\ Z c= Y /\ V; theorem :: XBOOLE_1:28 X c= Y implies X /\ Y = X; theorem :: XBOOLE_1:29 X /\ Y c= X \/ Z; theorem :: XBOOLE_1:30 X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z; theorem :: XBOOLE_1:31 (X /\ Y) \/ (X /\ Z) c= Y \/ Z; theorem :: XBOOLE_1:32 X \ Y = Y \ X implies X = Y; theorem :: XBOOLE_1:33 X c= Y implies X \ Z c= Y \ Z; theorem :: XBOOLE_1:34 X c= Y implies Z \ Y c= Z \ X; theorem :: XBOOLE_1:35 X c= Y & Z c= V implies X \ V c= Y \ Z; theorem :: XBOOLE_1:36 X \ Y c= X; theorem :: XBOOLE_1:37 X \ Y = {} iff X c= Y; theorem :: XBOOLE_1:38 X c= Y \ X implies X = {}; theorem :: XBOOLE_1:39 X \/ (Y \ X) = X \/ Y; theorem :: XBOOLE_1:40 (X \/ Y) \ Y = X \ Y; theorem :: XBOOLE_1:41 (X \ Y) \ Z = X \ (Y \/ Z); theorem :: XBOOLE_1:42 (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z); theorem :: XBOOLE_1:43 X c= Y \/ Z implies X \ Y c= Z; theorem :: XBOOLE_1:44 X \ Y c= Z implies X c= Y \/ Z; theorem :: XBOOLE_1:45 X c= Y implies Y = X \/ (Y \ X); theorem :: XBOOLE_1:46 X \ (X \/ Y) = {}; theorem :: XBOOLE_1:47 X \ X /\ Y = X \ Y; theorem :: XBOOLE_1:48 X \ (X \ Y) = X /\ Y; theorem :: XBOOLE_1:49 X /\ (Y \ Z) = (X /\ Y) \ Z; theorem :: XBOOLE_1:50 X /\ (Y \ Z) = X /\ Y \ X /\ Z; theorem :: XBOOLE_1:51 X /\ Y \/ (X \ Y) = X; theorem :: XBOOLE_1:52 X \ (Y \ Z) = (X \ Y) \/ X /\ Z; theorem :: XBOOLE_1:53 X \ (Y \/ Z) = (X \ Y) /\ (X \ Z); theorem :: XBOOLE_1:54 X \ (Y /\ Z) = (X \ Y) \/ (X \ Z); theorem :: XBOOLE_1:55 (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X); theorem :: XBOOLE_1:56 X c< Y & Y c< Z implies X c< Z; theorem :: XBOOLE_1:57 not (X c< Y & Y c< X); theorem :: XBOOLE_1:58 X c< Y & Y c= Z implies X c< Z; theorem :: XBOOLE_1:59 X c= Y & Y c< Z implies X c< Z; theorem :: XBOOLE_1:60 X c= Y implies not Y c< X; theorem :: XBOOLE_1:61 X <> {} implies {} c< X; theorem :: XBOOLE_1:62 not X c< {}; ::$N Modus Celarent ::$N Modus Darii theorem :: XBOOLE_1:63 X c= Y & Y misses Z implies X misses Z; theorem :: XBOOLE_1:64 A c= X & B c= Y & X misses Y implies A misses B; theorem :: XBOOLE_1:65 X misses {}; theorem :: XBOOLE_1:66 X meets X iff X <> {}; theorem :: XBOOLE_1:67 X c= Y & X c= Z & Y misses Z implies X = {}; ::$N Modus Darapti theorem :: XBOOLE_1:68 for A being non empty set st A c= Y & A c= Z holds Y meets Z; theorem :: XBOOLE_1:69 for A being non empty set st A c= Y holds A meets Y; theorem :: XBOOLE_1:70 X meets Y \/ Z iff X meets Y or X meets Z; theorem :: XBOOLE_1:71 X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z; theorem :: XBOOLE_1:72 X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9; theorem :: XBOOLE_1:73 X c= Y \/ Z & X misses Z implies X c= Y; theorem :: XBOOLE_1:74 X meets Y /\ Z implies X meets Y; theorem :: XBOOLE_1:75 X meets Y implies X /\ Y meets Y; theorem :: XBOOLE_1:76 Y misses Z implies X /\ Y misses X /\ Z; theorem :: XBOOLE_1:77 X meets Y & X c= Z implies X meets Y /\ Z; theorem :: XBOOLE_1:78 X misses Y implies X /\ (Y \/ Z) = X /\ Z; theorem :: XBOOLE_1:79 X \ Y misses Y; theorem :: XBOOLE_1:80 X misses Y implies X misses Y \ Z; theorem :: XBOOLE_1:81 X misses Y \ Z implies Y misses X \ Z; theorem :: XBOOLE_1:82 X \ Y misses Y \ X; theorem :: XBOOLE_1:83 X misses Y iff X \ Y = X; theorem :: XBOOLE_1:84 X meets Y & X misses Z implies X meets Y \ Z; theorem :: XBOOLE_1:85 X c= Y implies X misses Z \ Y; theorem :: XBOOLE_1:86 X c= Y & X misses Z implies X c= Y \ Z; theorem :: XBOOLE_1:87 Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y; theorem :: XBOOLE_1:88 X misses Y implies (X \/ Y) \ Y = X; theorem :: XBOOLE_1:89 X /\ Y misses X \ Y; theorem :: XBOOLE_1:90 X \ (X /\ Y) misses Y; theorem :: XBOOLE_1:91 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z); theorem :: XBOOLE_1:92 X \+\ X = {}; theorem :: XBOOLE_1:93 X \/ Y = (X \+\ Y) \/ X /\ Y; theorem :: XBOOLE_1:94 X \/ Y = X \+\ Y \+\ X /\ Y; theorem :: XBOOLE_1:95 X /\ Y = X \+\ Y \+\ (X \/ Y); theorem :: XBOOLE_1:96 X \ Y c= X \+\ Y; theorem :: XBOOLE_1:97 X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z; theorem :: XBOOLE_1:98 X \/ Y = X \+\ (Y \ X); theorem :: XBOOLE_1:99 (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)); theorem :: XBOOLE_1:100 X \ Y = X \+\ (X /\ Y); theorem :: XBOOLE_1:101 X \+\ Y = (X \/ Y) \ X /\ Y; theorem :: XBOOLE_1:102 X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z; theorem :: XBOOLE_1:103 X /\ Y misses X \+\ Y; theorem :: XBOOLE_1:104 X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable; begin :: Addenda theorem :: XBOOLE_1:105 for X, Y being set st X c< Y holds Y \ X <> {}; theorem :: XBOOLE_1:106 X c= A \ B implies X c= A & X misses B; theorem :: XBOOLE_1:107 X c= A \+\ B iff X c= A \/ B & X misses A /\ B; theorem :: XBOOLE_1:108 X c= A implies X /\ Y c= A; theorem :: XBOOLE_1:109 X c= A implies X \ Y c= A; theorem :: XBOOLE_1:110 X c= A & Y c= A implies X \+\ Y c= A; theorem :: XBOOLE_1:111 (X /\ Z) \ (Y /\ Z) = (X \ Y) /\ Z; theorem :: XBOOLE_1:112 (X /\ Z) \+\ (Y /\ Z) = (X \+\ Y) /\ Z; theorem :: XBOOLE_1:113 X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V); 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; ::$CT theorem :: XBOOLE_1:116 X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z); theorem :: XBOOLE_1:117 for P,G,C being set st C c= G holds P \ C = (P \ G) \/ (P /\ (G \ C));