Journal of Formalized Mathematics
EMM, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Boolean Properties of Sets --- Theorems

by
Library Committee

MML identifier: XBOOLE_1
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, ZFMISC_1;
notation TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
clusters XBOOLE_0;
requirements BOOLE;

begin

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

theorem :: XBOOLE_1:1  :: BOOLE'29:
X c= Y & Y c= Z implies X c= Z;

theorem :: XBOOLE_1:2  :: BOOLE'27:
{} c= X;

theorem :: XBOOLE_1:3  :: BOOLE'30:
X c= {} implies X = {};

:: \/

theorem :: XBOOLE_1:4  :: BOOLE'64:
(X \/ Y) \/ Z = X \/ (Y \/ Z);

theorem :: XBOOLE_1:5 :: SYSREL'2:
(X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z);

theorem :: XBOOLE_1:6 :: SYSREL'3:
X \/ (X \/ Y) = X \/ Y;

theorem :: XBOOLE_1:7  :: BOOLE'31:
X c= X \/ Y;

theorem :: XBOOLE_1:8  :: BOOLE'32:
X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: XBOOLE_1:9  :: BOOLE'33:
X c= Y implies X \/ Z c= Y \/ Z;

theorem :: XBOOLE_1:10 :: AMI_5'2:
X c= Y implies X c= Z \/ Y;

theorem :: XBOOLE_1:11 :: SETWISEO'7:
X \/ Y c= Z implies X c= Z;

theorem :: XBOOLE_1:12  :: BOOLE'35:
X c= Y implies X \/ Y = Y;

theorem :: XBOOLE_1:13 :: BOOLE'34:
X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: XBOOLE_1:14 :: BOOLE'56:
(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 :: BOOLE'59:
X \/ Y = {} implies X = {};

:: /\

theorem :: XBOOLE_1:16  :: BOOLE'67:
(X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: XBOOLE_1:17  :: BOOLE'37:
X /\ Y c= X;

theorem :: XBOOLE_1:18 :: SYSREL'4:
X c= Y /\ Z implies X c= Y;

theorem :: XBOOLE_1:19  :: BOOLE'39:
Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: XBOOLE_1:20 :: BOOLE'57:
(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 :: BOOLE'68:
X /\ (X \/ Y) = X;

theorem :: XBOOLE_1:22  :: BOOLE'69:
X \/ (X /\ Y) = X;

theorem :: XBOOLE_1:23  :: BOOLE'70:
X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: XBOOLE_1:24  :: BOOLE'71:
X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);

theorem :: XBOOLE_1:25 :: BOOLE'72:
(X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

theorem :: XBOOLE_1:26  :: BOOLE'40:
X c= Y implies X /\ Z c= Y /\ Z;

theorem :: XBOOLE_1:27 :: BOOLE'41:
X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: XBOOLE_1:28  :: BOOLE'42:
X c= Y implies X /\ Y = X;

theorem :: XBOOLE_1:29 :: BOOLE'38:
X /\ Y c= X \/ Z;

theorem :: XBOOLE_1:30 :: BOOLE'44:
X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: XBOOLE_1:31 :: BOOLE'53:
(X /\ Y) \/ (X /\ Z) c= Y \/ Z;

:: \

theorem :: XBOOLE_1:32 :: BOOLE'90:
X \ Y = Y \ X implies X = Y;

theorem :: XBOOLE_1:33  :: BOOLE'46:
X c= Y implies X \ Z c= Y \ Z;

theorem :: XBOOLE_1:34  :: BOOLE'47:
X c= Y implies Z \ Y c= Z \ X;

theorem :: XBOOLE_1:35 :: BOOLE'48:
X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: XBOOLE_1:36  :: BOOLE'49:
X \ Y c= X;

theorem :: XBOOLE_1:37 :: BOOLE'45:
X \ Y = {} iff X c= Y;

theorem :: XBOOLE_1:38 :: BOOLE'50:
X c= Y \ X implies X = {};

theorem :: XBOOLE_1:39  :: BOOLE'79:
X \/ (Y \ X) = X \/ Y;

theorem :: XBOOLE_1:40 :: BOOLE'83:
(X \/ Y) \ Y = X \ Y;

theorem :: XBOOLE_1:41  :: BOOLE'88:
(X \ Y) \ Z = X \ (Y \/ Z);

theorem :: XBOOLE_1:42  :: BOOLE'89:
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: XBOOLE_1:43 :: BOOLE'52:
X c= Y \/ Z implies X \ Y c= Z;

theorem :: XBOOLE_1:44 :: NORMFORM'2:
X \ Y c= Z implies X c= Y \/ Z;

theorem :: XBOOLE_1:45 :: BOOLE'54:
X c= Y implies Y = X \/ (Y \ X);

theorem :: XBOOLE_1:46 :: BOOLE'76:
X \ (X \/ Y) = {};

theorem :: XBOOLE_1:47  :: BOOLE'77:
X \ X /\ Y = X \ Y;

theorem :: XBOOLE_1:48 :: BOOLE'82:
X \ (X \ Y) = X /\ Y;

theorem :: XBOOLE_1:49  :: BOOLE'116:
X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: XBOOLE_1:50  :: BOOLE'117
X /\ (Y \ Z) = X /\ Y \ X /\ Z;

theorem :: XBOOLE_1:51  :: BOOLE'80:
X /\ Y \/ (X \ Y) = X;

theorem :: XBOOLE_1:52  :: BOOLE'81:
X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: XBOOLE_1:53 :: BOOLE'85:
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: XBOOLE_1:54  :: BOOLE'86:
X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: XBOOLE_1:55  :: BOOLE'87:
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: XBOOLE_1:56 :: BOOLE'123:
X c< Y & Y c< Z implies X c< Z;

theorem :: XBOOLE_1:57 :: BOOLE'126:
not (X c< Y & Y c< X);

theorem :: XBOOLE_1:58 :: BOOLE'121:
X c< Y & Y c= Z implies X c< Z;

theorem :: XBOOLE_1:59 :: BOOLE'122:
X c= Y & Y c< Z implies X c< Z;

theorem :: XBOOLE_1:60  :: BOOLE'127:
X c= Y implies not Y c< X;

theorem :: XBOOLE_1:61 :: BOOLE'124:
X <> {} implies {} c< X;

theorem :: XBOOLE_1:62 :: BOOLE'125:
not X c< {};

:: meets & misses

theorem :: XBOOLE_1:63  :: BOOLE'55:
X c= Y & Y misses Z implies X misses Z;

theorem :: XBOOLE_1:64 :: AMI_5'1:
A c= X & B c= Y & X misses Y implies A misses B;

theorem :: XBOOLE_1:65 :: BOOLE'104:
X misses {};

theorem :: XBOOLE_1:66 :: BOOLE'110:
X meets X iff X <> {};

theorem :: XBOOLE_1:67 :: BOOLE'51:
X c= Y & X c= Z & Y misses Z implies X = {};

theorem :: XBOOLE_1:68 :: JORDAN9'2:
for A being non empty set st A c= Y & A c= Z holds Y meets Z;

theorem :: XBOOLE_1:69 :: TOPREAL6'27:
for A being non empty set st A c= Y holds A meets Y;

theorem :: XBOOLE_1:70  :: BOOLE'100:
X meets Y \/ Z iff X meets Y or X meets Z;

theorem :: XBOOLE_1:71 :: TOPREAL6'28:
X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z;

theorem :: XBOOLE_1:72 :: SETWISEO'9:
X' \/ Y' = X \/ Y & X misses X' & Y misses Y' implies X = Y';

theorem :: XBOOLE_1:73 :: BOOLE'120:
X c= Y \/ Z & X misses Z implies X c= Y;

theorem :: XBOOLE_1:74  :: BOOLE'102:
X meets Y /\ Z implies X meets Y;

theorem :: XBOOLE_1:75 :: JORDAN9'1:
X meets Y implies X /\ Y meets Y;

theorem :: XBOOLE_1:76 :: PROB_2'7:
Y misses Z implies X /\ Y misses X /\ Z;

theorem :: XBOOLE_1:77 :: BORSUK_1'1:
X meets Y & X c= Z implies X meets Y /\ Z;

theorem :: XBOOLE_1:78 :: SPRECT_3'1:
X misses Y implies X /\ (Y \/ Z) = X /\ Z;

theorem :: XBOOLE_1:79  :: BOOLE'78:
X \ Y misses Y;

theorem :: XBOOLE_1:80 :: BOOLE'113:
X misses Y implies X misses Y \ Z;

theorem :: XBOOLE_1:81 :: AMI_1'12:
X misses Y \ Z implies Y misses X \ Z;

theorem :: XBOOLE_1:82 :: RLVECT_2'102:
X \ Y misses Y \ X;

theorem :: XBOOLE_1:83  :: BOOLE'84:
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 :: DYNKIN'3:
X c= Y implies X misses Z \ Y;

theorem :: XBOOLE_1:86  :: JCT_MISC'1:
X c= Y & X misses Z implies X c= Y \ Z;

theorem :: XBOOLE_1:87 :: CQC_THE3'60:
Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y;

theorem :: XBOOLE_1:88  :: FINSUB_1'2:
X misses Y implies (X \/ Y) \ Y = X;

theorem :: XBOOLE_1:89  :: BOOLE'111:
X /\ Y misses X \ Y;

theorem :: XBOOLE_1:90
X \ (X /\ Y) misses Y;

:: \+\

theorem :: XBOOLE_1:91 :: BOOLE'99:
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: XBOOLE_1:92 :: BOOLE'93:
X \+\ X = {};

theorem :: XBOOLE_1:93  :: BOOLE'95:
X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: XBOOLE_1:94 :: FINSUB_1'4:
X \/ Y = X \+\ Y \+\ X /\ Y;

theorem :: XBOOLE_1:95 :: FINSUB_1'6:
X /\ Y = X \+\ Y \+\ (X \/ Y);

theorem :: XBOOLE_1:96 :: BOOLE'58:
X \ Y c= X \+\ Y;

theorem :: XBOOLE_1:97 :: BOOLE'115:
X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: XBOOLE_1:98 :: FINSUB_1'3:
X \/ Y = X \+\ (Y \ X);

theorem :: XBOOLE_1:99 :: BOOLE'97:
(X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: XBOOLE_1:100 :: FINSUB_1'5:
X \ Y = X \+\ (X /\ Y);

theorem :: XBOOLE_1:101 :: BOOLE'96:
X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: XBOOLE_1:102 :: BOOLE'98:
X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: XBOOLE_1:103 :: BOOLE'112:
X /\ Y misses X \+\ Y;

:: comparable

theorem :: XBOOLE_1:104 :: TREES_1'20:
X c< Y or X = Y or Y c< X iff X,Y are_c=-comparable;

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

theorem :: XBOOLE_1:106  :: ZFMISC_1:85
X c= A \ B implies X c= A & X misses B;

theorem :: XBOOLE_1:107 :: ZFMISC_1:87
X c= A \+\ B iff X c= A \/ B & X misses A /\ B;

theorem :: XBOOLE_1:108 :: ZFMISC_1:89
X c= A implies X /\ Y c= A;

theorem :: XBOOLE_1:109  :: ZFMISC_1:90
X c= A implies X \ Y c= A;

theorem :: XBOOLE_1:110 :: ZFMISC_1:91
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;