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; begin :: Addenda 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; begin :: additional theorem :: XBOOLE_1:113 :: from BORSUK_5 X \/ Y \/ Z \/ V = X \/ (Y \/ Z \/ V);