:: XBOOLE_1 semantic presentation

theorem Th1: :: XBOOLE_1:1

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ c= b₃ holds
b₁ c= b₃

proof end;

theorem Th2: :: XBOOLE_1:2

for b₁ being set holds {} c= b₁

proof end;

theorem Th3: :: XBOOLE_1:3

for b₁ being set st b₁ c= {} holds
b₁ = {}

proof end;

theorem Th4: :: XBOOLE_1:4

for b₁, b₂, b₃ being set holds (b₁ \/ b₂) \/ b₃ = b₁ \/ (b₂ \/ b₃)

proof end;

theorem Th5: :: XBOOLE_1:5

for b₁, b₂, b₃ being set holds (b₁ \/ b₂) \/ b₃ = (b₁ \/ b₃) \/ (b₂ \/ b₃)

proof end;

theorem Th6: :: XBOOLE_1:6

for b₁, b₂ being set holds b₁ \/ (b₁ \/ b₂) = b₁ \/ b₂

proof end;

theorem Th7: :: XBOOLE_1:7

for b₁, b₂ being set holds b₁ c= b₁ \/ b₂

proof end;

theorem Th8: :: XBOOLE_1:8

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₃ c= b₂ holds
b₁ \/ b₃ c= b₂

proof end;

theorem Th9: :: XBOOLE_1:9

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ \/ b₃ c= b₂ \/ b₃

proof end;

theorem Th10: :: XBOOLE_1:10

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ c= b₃ \/ b₂

proof end;

theorem Th11: :: XBOOLE_1:11

for b₁, b₂, b₃ being set st b₁ \/ b₂ c= b₃ holds
b₁ c= b₃

proof end;

theorem Th12: :: XBOOLE_1:12

for b₁, b₂ being set st b₁ c= b₂ holds
b₁ \/ b₂ = b₂

proof end;

theorem Th13: :: XBOOLE_1:13

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
b₁ \/ b₃ c= b₂ \/ b₄

proof end;

theorem Th14: :: XBOOLE_1:14

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₃ c= b₂ & ( for b₄ being set st b₁ c= b₄ & b₃ c= b₄ holds
b₂ c= b₄ ) holds
b₂ = b₁ \/ b₃

proof end;

theorem Th15: :: XBOOLE_1:15

for b₁, b₂ being set st b₁ \/ b₂ = {} holds
b₁ = {}

proof end;

theorem Th16: :: XBOOLE_1:16

for b₁, b₂, b₃ being set holds (b₁ /\ b₂) /\ b₃ = b₁ /\ (b₂ /\ b₃)

proof end;

theorem Th17: :: XBOOLE_1:17

for b₁, b₂ being set holds b₁ /\ b₂ c= b₁

proof end;

theorem Th18: :: XBOOLE_1:18

for b₁, b₂, b₃ being set st b₁ c= b₂ /\ b₃ holds
b₁ c= b₂

proof end;

theorem Th19: :: XBOOLE_1:19

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₁ c= b₃ holds
b₁ c= b₂ /\ b₃

proof end;

theorem Th20: :: XBOOLE_1:20

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₁ c= b₃ & ( for b₄ being set st b₄ c= b₂ & b₄ c= b₃ holds
b₄ c= b₁ ) holds
b₁ = b₂ /\ b₃

proof end;

theorem Th21: :: XBOOLE_1:21

for b₁, b₂ being set holds b₁ /\ (b₁ \/ b₂) = b₁

proof end;

theorem Th22: :: XBOOLE_1:22

for b₁, b₂ being set holds b₁ \/ (b₁ /\ b₂) = b₁

proof end;

theorem Th23: :: XBOOLE_1:23

for b₁, b₂, b₃ being set holds b₁ /\ (b₂ \/ b₃) = (b₁ /\ b₂) \/ (b₁ /\ b₃)

proof end;

theorem Th24: :: XBOOLE_1:24

for b₁, b₂, b₃ being set holds b₁ \/ (b₂ /\ b₃) = (b₁ \/ b₂) /\ (b₁ \/ b₃)

proof end;

theorem Th25: :: XBOOLE_1:25

for b₁, b₂, b₃ being set holds ((b₁ /\ b₂) \/ (b₂ /\ b₃)) \/ (b₃ /\ b₁) = ((b₁ \/ b₂) /\ (b₂ \/ b₃)) /\ (b₃ \/ b₁)

proof end;

theorem Th26: :: XBOOLE_1:26

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ /\ b₃ c= b₂ /\ b₃

proof end;

theorem Th27: :: XBOOLE_1:27

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
b₁ /\ b₃ c= b₂ /\ b₄

proof end;

theorem Th28: :: XBOOLE_1:28

for b₁, b₂ being set st b₁ c= b₂ holds
b₁ /\ b₂ = b₁

proof end;

theorem Th29: :: XBOOLE_1:29

for b₁, b₂, b₃ being set holds b₁ /\ b₂ c= b₁ \/ b₃

proof end;

theorem Th30: :: XBOOLE_1:30

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ \/ (b₃ /\ b₂) = (b₁ \/ b₃) /\ b₂

proof end;

theorem Th31: :: XBOOLE_1:31

for b₁, b₂, b₃ being set holds (b₁ /\ b₂) \/ (b₁ /\ b₃) c= b₂ \/ b₃

proof end;

Lemma17: for b₁, b₂ being set holds
( b₁ \ b₂ = {} iff b₁ c= b₂ )

proof end;

theorem Th32: :: XBOOLE_1:32

for b₁, b₂ being set st b₁ \ b₂ = b₂ \ b₁ holds
b₁ = b₂

proof end;

theorem Th33: :: XBOOLE_1:33

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ \ b₃ c= b₂ \ b₃

proof end;

theorem Th34: :: XBOOLE_1:34

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₃ \ b₂ c= b₃ \ b₁

proof end;

Lemma20: for b₁, b₂, b₃ being set holds b₁ \ (b₂ /\ b₃) = (b₁ \ b₂) \/ (b₁ \ b₃)

proof end;

theorem Th35: :: XBOOLE_1:35

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ holds
b₁ \ b₄ c= b₂ \ b₃

proof end;

theorem Th36: :: XBOOLE_1:36

for b₁, b₂ being set holds b₁ \ b₂ c= b₁

proof end;

theorem Th37: :: XBOOLE_1:37

for b₁, b₂ being set holds
( b₁ \ b₂ = {} iff b₁ c= b₂ ) by Lemma17;

theorem Th38: :: XBOOLE_1:38

for b₁, b₂ being set st b₁ c= b₂ \ b₁ holds
b₁ = {}

proof end;

theorem Th39: :: XBOOLE_1:39

for b₁, b₂ being set holds b₁ \/ (b₂ \ b₁) = b₁ \/ b₂

proof end;

theorem Th40: :: XBOOLE_1:40

for b₁, b₂ being set holds (b₁ \/ b₂) \ b₂ = b₁ \ b₂

proof end;

theorem Th41: :: XBOOLE_1:41

for b₁, b₂, b₃ being set holds (b₁ \ b₂) \ b₃ = b₁ \ (b₂ \/ b₃)

proof end;

theorem Th42: :: XBOOLE_1:42

for b₁, b₂, b₃ being set holds (b₁ \/ b₂) \ b₃ = (b₁ \ b₃) \/ (b₂ \ b₃)

proof end;

theorem Th43: :: XBOOLE_1:43

for b₁, b₂, b₃ being set st b₁ c= b₂ \/ b₃ holds
b₁ \ b₂ c= b₃

proof end;

theorem Th44: :: XBOOLE_1:44

for b₁, b₂, b₃ being set st b₁ \ b₂ c= b₃ holds
b₁ c= b₂ \/ b₃

proof end;

theorem Th45: :: XBOOLE_1:45

for b₁, b₂ being set st b₁ c= b₂ holds
b₂ = b₁ \/ (b₂ \ b₁)

proof end;

theorem Th46: :: XBOOLE_1:46

for b₁, b₂ being set holds b₁ \ (b₁ \/ b₂) = {}

proof end;

theorem Th47: :: XBOOLE_1:47

for b₁, b₂ being set holds b₁ \ (b₁ /\ b₂) = b₁ \ b₂

proof end;

theorem Th48: :: XBOOLE_1:48

for b₁, b₂ being set holds b₁ \ (b₁ \ b₂) = b₁ /\ b₂

proof end;

theorem Th49: :: XBOOLE_1:49

for b₁, b₂, b₃ being set holds b₁ /\ (b₂ \ b₃) = (b₁ /\ b₂) \ b₃

proof end;

theorem Th50: :: XBOOLE_1:50

for b₁, b₂, b₃ being set holds b₁ /\ (b₂ \ b₃) = (b₁ /\ b₂) \ (b₁ /\ b₃)

proof end;

theorem Th51: :: XBOOLE_1:51

for b₁, b₂ being set holds (b₁ /\ b₂) \/ (b₁ \ b₂) = b₁

proof end;

theorem Th52: :: XBOOLE_1:52

for b₁, b₂, b₃ being set holds b₁ \ (b₂ \ b₃) = (b₁ \ b₂) \/ (b₁ /\ b₃)

proof end;

theorem Th53: :: XBOOLE_1:53

for b₁, b₂, b₃ being set holds b₁ \ (b₂ \/ b₃) = (b₁ \ b₂) /\ (b₁ \ b₃)

proof end;

theorem Th54: :: XBOOLE_1:54

for b₁, b₂, b₃ being set holds b₁ \ (b₂ /\ b₃) = (b₁ \ b₂) \/ (b₁ \ b₃) by Lemma20;

theorem Th55: :: XBOOLE_1:55

for b₁, b₂ being set holds (b₁ \/ b₂) \ (b₁ /\ b₂) = (b₁ \ b₂) \/ (b₂ \ b₁)

proof end;

Lemma31: for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ c< b₃ holds
b₁ c< b₃

proof end;

theorem Th56: :: XBOOLE_1:56

for b₁, b₂, b₃ being set st b₁ c< b₂ & b₂ c< b₃ holds
b₁ c< b₃

proof end;

theorem Th57: :: XBOOLE_1:57

for b₁, b₂ being set holds
( not b₁ c< b₂ or not b₂ c< b₁ ) ;

theorem Th58: :: XBOOLE_1:58

for b₁, b₂, b₃ being set st b₁ c< b₂ & b₂ c= b₃ holds
b₁ c< b₃

proof end;

theorem Th59: :: XBOOLE_1:59

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ c< b₃ holds
b₁ c< b₃ by Lemma31;

theorem Th60: :: XBOOLE_1:60

for b₁, b₂ being set st b₁ c= b₂ holds
not b₂ c< b₁

proof end;

theorem Th61: :: XBOOLE_1:61

for b₁ being set st b₁ <> {} holds
{} c< b₁

proof end;

theorem Th62: :: XBOOLE_1:62

for b₁ being set holds not b₁ c< {}

proof end;

theorem Th63: :: XBOOLE_1:63

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₂ misses b₃ holds
b₁ misses b₃

proof end;

theorem Th64: :: XBOOLE_1:64

for b₁, b₂, b₃, b₄ being set st b₁ c= b₂ & b₃ c= b₄ & b₂ misses b₄ holds
b₁ misses b₃

proof end;

theorem Th65: :: XBOOLE_1:65

for b₁ being set holds b₁ misses {}

proof end;

theorem Th66: :: XBOOLE_1:66

for b₁ being set holds
( b₁ meets b₁ iff b₁ <> {} )

proof end;

theorem Th67: :: XBOOLE_1:67

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₁ c= b₃ & b₂ misses b₃ holds
b₁ = {}

proof end;

theorem Th68: :: XBOOLE_1:68

for b₁, b₂ being set
for b₃ being non empty set st b₃ c= b₁ & b₃ c= b₂ holds
b₁ meets b₂

proof end;

theorem Th69: :: XBOOLE_1:69

for b₁ being set
for b₂ being non empty set st b₂ c= b₁ holds
b₂ meets b₁

proof end;

theorem Th70: :: XBOOLE_1:70

for b₁, b₂, b₃ being set holds
( ( b₁ meets b₂ or b₁ meets b₃ ) iff b₁ meets b₂ \/ b₃ )

proof end;

theorem Th71: :: XBOOLE_1:71

for b₁, b₂, b₃ being set st b₁ \/ b₂ = b₃ \/ b₂ & b₁ misses b₂ & b₃ misses b₂ holds
b₁ = b₃

proof end;

theorem Th72: :: XBOOLE_1:72

for b₁, b₂, b₃, b₄ being set st b₁ \/ b₂ = b₃ \/ b₄ & b₃ misses b₁ & b₄ misses b₂ holds
b₃ = b₂

proof end;

theorem Th73: :: XBOOLE_1:73

for b₁, b₂, b₃ being set st b₁ c= b₂ \/ b₃ & b₁ misses b₃ holds
b₁ c= b₂

proof end;

theorem Th74: :: XBOOLE_1:74

for b₁, b₂, b₃ being set st b₁ meets b₂ /\ b₃ holds
b₁ meets b₂

proof end;

theorem Th75: :: XBOOLE_1:75

for b₁, b₂ being set st b₁ meets b₂ holds
b₁ /\ b₂ meets b₂

proof end;

theorem Th76: :: XBOOLE_1:76

for b₁, b₂, b₃ being set st b₁ misses b₂ holds
b₃ /\ b₁ misses b₃ /\ b₂

proof end;

theorem Th77: :: XBOOLE_1:77

for b₁, b₂, b₃ being set st b₁ meets b₂ & b₁ c= b₃ holds
b₁ meets b₂ /\ b₃

proof end;

theorem Th78: :: XBOOLE_1:78

for b₁, b₂, b₃ being set st b₁ misses b₂ holds
b₁ /\ (b₂ \/ b₃) = b₁ /\ b₃

proof end;

theorem Th79: :: XBOOLE_1:79

for b₁, b₂ being set holds b₁ \ b₂ misses b₂

proof end;

theorem Th80: :: XBOOLE_1:80

for b₁, b₂, b₃ being set st b₁ misses b₂ holds
b₁ misses b₂ \ b₃

proof end;

theorem Th81: :: XBOOLE_1:81

for b₁, b₂, b₃ being set st b₁ misses b₂ \ b₃ holds
b₂ misses b₁ \ b₃

proof end;

theorem Th82: :: XBOOLE_1:82

for b₁, b₂ being set holds b₁ \ b₂ misses b₂ \ b₁

proof end;

theorem Th83: :: XBOOLE_1:83

for b₁, b₂ being set holds
( b₁ misses b₂ iff b₁ \ b₂ = b₁ )

proof end;

theorem Th84: :: XBOOLE_1:84

for b₁, b₂, b₃ being set st b₁ meets b₂ & b₁ misses b₃ holds
b₁ meets b₂ \ b₃

proof end;

theorem Th85: :: XBOOLE_1:85

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ misses b₃ \ b₂

proof end;

theorem Th86: :: XBOOLE_1:86

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₁ misses b₃ holds
b₁ c= b₂ \ b₃

proof end;

theorem Th87: :: XBOOLE_1:87

for b₁, b₂, b₃ being set st b₁ misses b₂ holds
(b₃ \ b₁) \/ b₂ = (b₃ \/ b₂) \ b₁

proof end;

theorem Th88: :: XBOOLE_1:88

for b₁, b₂ being set st b₁ misses b₂ holds
(b₁ \/ b₂) \ b₂ = b₁

proof end;

theorem Th89: :: XBOOLE_1:89

for b₁, b₂ being set holds b₁ /\ b₂ misses b₁ \ b₂

proof end;

theorem Th90: :: XBOOLE_1:90

for b₁, b₂ being set holds b₁ \ (b₁ /\ b₂) misses b₂

proof end;

theorem Th91: :: XBOOLE_1:91

for b₁, b₂, b₃ being set holds (b₁ \+\ b₂) \+\ b₃ = b₁ \+\ (b₂ \+\ b₃)

proof end;

theorem Th92: :: XBOOLE_1:92

for b₁ being set holds b₁ \+\ b₁ = {} by Lemma17;

theorem Th93: :: XBOOLE_1:93

for b₁, b₂ being set holds b₁ \/ b₂ = (b₁ \+\ b₂) \/ (b₁ /\ b₂)

proof end;

Lemma42: for b₁, b₂ being set holds b₁ /\ b₂ misses b₁ \+\ b₂

proof end;

Lemma43: for b₁, b₂ being set holds b₁ \+\ b₂ = (b₁ \/ b₂) \ (b₁ /\ b₂)

proof end;

theorem Th94: :: XBOOLE_1:94

for b₁, b₂ being set holds b₁ \/ b₂ = (b₁ \+\ b₂) \+\ (b₁ /\ b₂)

proof end;

theorem Th95: :: XBOOLE_1:95

for b₁, b₂ being set holds b₁ /\ b₂ = (b₁ \+\ b₂) \+\ (b₁ \/ b₂)

proof end;

theorem Th96: :: XBOOLE_1:96

for b₁, b₂ being set holds b₁ \ b₂ c= b₁ \+\ b₂ by Th7;

theorem Th97: :: XBOOLE_1:97

for b₁, b₂, b₃ being set st b₁ \ b₂ c= b₃ & b₂ \ b₁ c= b₃ holds
b₁ \+\ b₂ c= b₃ by Th8;

theorem Th98: :: XBOOLE_1:98

for b₁, b₂ being set holds b₁ \/ b₂ = b₁ \+\ (b₂ \ b₁)

proof end;

theorem Th99: :: XBOOLE_1:99

for b₁, b₂, b₃ being set holds (b₁ \+\ b₂) \ b₃ = (b₁ \ (b₂ \/ b₃)) \/ (b₂ \ (b₁ \/ b₃))

proof end;

theorem Th100: :: XBOOLE_1:100

for b₁, b₂ being set holds b₁ \ b₂ = b₁ \+\ (b₁ /\ b₂)

proof end;

theorem Th101: :: XBOOLE_1:101

for b₁, b₂ being set holds b₁ \+\ b₂ = (b₁ \/ b₂) \ (b₁ /\ b₂) by Lemma43;

theorem Th102: :: XBOOLE_1:102

for b₁, b₂, b₃ being set holds b₁ \ (b₂ \+\ b₃) = (b₁ \ (b₂ \/ b₃)) \/ ((b₁ /\ b₂) /\ b₃)

proof end;

theorem Th103: :: XBOOLE_1:103

for b₁, b₂ being set holds b₁ /\ b₂ misses b₁ \+\ b₂ by Lemma42;

theorem Th104: :: XBOOLE_1:104

for b₁, b₂ being set holds
( ( b₁ c< b₂ or b₁ = b₂ or b₂ c< b₁ ) iff b₁,b₂ are_c=-comparable )

proof end;

theorem Th105: :: XBOOLE_1:105

for b₁, b₂ being set st b₁ c< b₂ holds
b₂ \ b₁ <> {}

proof end;

theorem Th106: :: XBOOLE_1:106

for b₁, b₂, b₃ being set st b₁ c= b₂ \ b₃ holds
( b₁ c= b₂ & b₁ misses b₃ )

proof end;

theorem Th107: :: XBOOLE_1:107

for b₁, b₂, b₃ being set holds
( b₁ c= b₂ \+\ b₃ iff ( b₁ c= b₂ \/ b₃ & b₁ misses b₂ /\ b₃ ) )

proof end;

theorem Th108: :: XBOOLE_1:108

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ /\ b₃ c= b₂

proof end;

theorem Th109: :: XBOOLE_1:109

for b₁, b₂, b₃ being set st b₁ c= b₂ holds
b₁ \ b₃ c= b₂

proof end;

theorem Th110: :: XBOOLE_1:110

for b₁, b₂, b₃ being set st b₁ c= b₂ & b₃ c= b₂ holds
b₁ \+\ b₃ c= b₂

proof end;

theorem Th111: :: XBOOLE_1:111

for b₁, b₂, b₃ being set holds (b₁ /\ b₂) \ (b₃ /\ b₂) = (b₁ \ b₃) /\ b₂

proof end;

theorem Th112: :: XBOOLE_1:112

for b₁, b₂, b₃ being set holds (b₁ /\ b₂) \+\ (b₃ /\ b₂) = (b₁ \+\ b₃) /\ b₂

proof end;

theorem Th113: :: XBOOLE_1:113

for b₁, b₂, b₃, b₄ being set holds ((b₁ \/ b₂) \/ b₃) \/ b₄ = b₁ \/ ((b₂ \/ b₃) \/ b₄)

proof end;

theorem Th114: :: XBOOLE_1:114

for b₁, b₂, b₃, b₄ being set st b₁ misses b₄ & b₂ misses b₄ & b₃ misses b₄ holds
(b₁ \/ b₂) \/ b₃ misses b₄

proof end;