:: YELLOW_5 semantic presentation

theorem Th1: :: YELLOW_5:1

for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂ being Element of b₁ holds b₂ "\/" b₂ = b₂

proof end;

theorem Th2: :: YELLOW_5:2

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Element of b₁ holds b₂ "/\" b₂ = b₂

proof end;

theorem Th3: :: YELLOW_5:3

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ "\/" b₃ <= b₄ holds
b₂ <= b₄

proof end;

theorem Th4: :: YELLOW_5:4

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₄ <= b₂ "/\" b₃ holds
b₄ <= b₂

proof end;

theorem Th5: :: YELLOW_5:5

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" b₃ <= b₂ "\/" b₄

proof end;

theorem Th6: :: YELLOW_5:6

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₂ "/\" b₄ <= b₃ "/\" b₄

proof end;

theorem Th7: :: YELLOW_5:7

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₂ "\/" b₄ <= b₃ "\/" b₄

proof end;

theorem Th8: :: YELLOW_5:8

for b₁ being sup-Semilattice
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
b₂ "\/" b₃ = b₃

proof end;

theorem Th9: :: YELLOW_5:9

for b₁ being sup-Semilattice
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₄ & b₃ <= b₄ holds
b₂ "\/" b₃ <= b₄

proof end;

theorem Th10: :: YELLOW_5:10

for b₁ being Semilattice
for b₂, b₃ being Element of b₁ st b₃ <= b₂ holds
b₂ "/\" b₃ = b₃

proof end;

theorem Th11: :: YELLOW_5:11

for b₁ being Boolean LATTICE
for b₂, b₃ being Element of b₁ holds
( b₃ is_a_complement_of b₂ iff b₃ = 'not' b₂ )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
func c₂ \ c₃ -> Element of a₁ equals :: YELLOW_5:def 1
a₂ "/\" ('not' a₃);
correctness ;

end;

:: deftheorem Def1 defines \ YELLOW_5:def 1 :

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
func c₂ \+\ c₃ -> Element of a₁ equals :: YELLOW_5:def 2
(a₂ \ a₃) "\/" (a₃ \ a₂);
correctness ;

end;

:: deftheorem Def2 defines \+\ YELLOW_5:def 2 :

Lemma8: for b₁ being antisymmetric with_suprema with_infima RelStr
for b₂, b₃ being Element of b₁ holds b₂ \+\ b₃ = b₃ \+\ b₂

proof end;

definition

let c₁ be antisymmetric with_suprema with_infima RelStr ;
let c₂, c₃ be Element of c₁;
redefine func \+\ as c₂ \+\ c₃ -> Element of a₁;
commutativity by Lemma8;

end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
pred c₂ meets c₃ means :Def3: :: YELLOW_5:def 3
a₂ "/\" a₃ <> Bottom a₁;

end;

:: deftheorem Def3 defines meets YELLOW_5:def 3 :

notation

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
antonym c₂ misses c₃ for c₂ meets c₃;

end;

notation

let c₁ be antisymmetric with_infima RelStr ;
let c₂, c₃ be Element of c₁;
antonym c₂ misses c₃ for c₂ meets c₃;

end;

definition

let c₁ be antisymmetric with_infima RelStr ;
let c₂, c₃ be Element of c₁;
redefine pred meets as c₂ meets c₃;
symmetry

proof end;

end;

theorem Th12: :: YELLOW_5:12

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₄ holds
b₂ \ b₃ <= b₄

proof end;

theorem Th13: :: YELLOW_5:13

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₂ \ b₄ <= b₃ \ b₄ by Th6;

theorem Th14: :: YELLOW_5:14

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ <= b₂ by YELLOW_0:23;

theorem Th15: :: YELLOW_5:15

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ <= b₂ \+\ b₃ by YELLOW_0:22;

theorem Th16: :: YELLOW_5:16

for b₁ being LATTICE
for b₂, b₃, b₄ being Element of b₁ st b₂ \ b₃ <= b₄ & b₃ \ b₂ <= b₄ holds
b₂ \+\ b₃ <= b₄ by Th9;

theorem Th17: :: YELLOW_5:17

for b₁ being LATTICE
for b₂ being Element of b₁ holds
( b₂ meets b₂ iff b₂ <> Bottom b₁ )

proof end;

theorem Th18: :: YELLOW_5:18

for b₁ being transitive antisymmetric with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" (b₃ \ b₄) = (b₂ "/\" b₃) \ b₄ by LATTICE3:16;

theorem Th19: :: YELLOW_5:19

for b₁ being transitive antisymmetric with_infima RelStr st b₁ is distributive holds
for b₂, b₃, b₄ being Element of b₁ st (b₂ "/\" b₃) "\/" (b₂ "/\" b₄) = b₂ holds
b₂ <= b₃ "\/" b₄

proof end;

theorem Th20: :: YELLOW_5:20

for b₁ being LATTICE st b₁ is distributive holds
for b₂, b₃, b₄ being Element of b₁ holds b₂ "\/" (b₃ "/\" b₄) = (b₂ "\/" b₃) "/\" (b₂ "\/" b₄)

proof end;

theorem Th21: :: YELLOW_5:21

for b₁ being LATTICE st b₁ is distributive holds
for b₂, b₃, b₄ being Element of b₁ holds (b₂ "\/" b₃) \ b₄ = (b₂ \ b₄) "\/" (b₃ \ b₄)

proof end;

theorem Th22: :: YELLOW_5:22

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being Element of b₁ st b₂ <= Bottom b₁ holds
b₂ = Bottom b₁

proof end;

theorem Th23: :: YELLOW_5:23

for b₁ being lower-bounded Semilattice
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ & b₂ <= b₄ & b₃ "/\" b₄ = Bottom b₁ holds
b₂ = Bottom b₁

proof end;

theorem Th24: :: YELLOW_5:24

for b₁ being antisymmetric lower-bounded with_suprema RelStr
for b₂, b₃ being Element of b₁ st b₂ "\/" b₃ = Bottom b₁ holds
( b₂ = Bottom b₁ & b₃ = Bottom b₁ )

proof end;

theorem Th25: :: YELLOW_5:25

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ & b₃ "/\" b₄ = Bottom b₁ holds
b₂ "/\" b₄ = Bottom b₁

proof end;

theorem Th26: :: YELLOW_5:26

for b₁ being lower-bounded Semilattice
for b₂ being Element of b₁ holds (Bottom b₁) \ b₂ = Bottom b₁

proof end;

theorem Th27: :: YELLOW_5:27

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ & b₃ <= b₄ holds
b₂ meets b₄

proof end;

theorem Th28: :: YELLOW_5:28

for b₁ being antisymmetric lower-bounded with_infima RelStr
for b₂ being Element of b₁ holds b₂ "/\" (Bottom b₁) = Bottom b₁

proof end;

theorem Th29: :: YELLOW_5:29

for b₁ being transitive antisymmetric lower-bounded with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ "/\" b₄ holds
b₂ meets b₃

proof end;

theorem Th30: :: YELLOW_5:30

for b₁ being transitive antisymmetric lower-bounded with_suprema with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ meets b₃ \ b₄ holds
b₂ meets b₃

proof end;

theorem Th31: :: YELLOW_5:31

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂ being Element of b₁ holds b₂ misses Bottom b₁

proof end;

theorem Th32: :: YELLOW_5:32

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ misses b₄ & b₃ <= b₄ holds
b₂ misses b₃

proof end;

theorem Th33: :: YELLOW_5:33

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st ( b₂ misses b₃ or b₂ misses b₄ ) holds
b₂ misses b₃ "/\" b₄

proof end;

theorem Th34: :: YELLOW_5:34

for b₁ being lower-bounded LATTICE
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ & b₂ <= b₄ & b₃ misses b₄ holds
b₂ = Bottom b₁

proof end;

theorem Th35: :: YELLOW_5:35

for b₁ being transitive antisymmetric lower-bounded with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ misses b₃ holds
b₂ "/\" b₄ misses b₃ "/\" b₄

proof end;

theorem Th36: :: YELLOW_5:36

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ "/\" b₃) "\/" (b₃ "/\" b₄)) "\/" (b₄ "/\" b₂) = ((b₂ "\/" b₃) "/\" (b₃ "\/" b₄)) "/\" (b₄ "\/" b₂)

proof end;

theorem Th37: :: YELLOW_5:37

for b₁ being non empty Boolean RelStr
for b₂ being Element of b₁ holds
( b₂ "/\" ('not' b₂) = Bottom b₁ & b₂ "\/" ('not' b₂) = Top b₁ )

proof end;

theorem Th38: :: YELLOW_5:38

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ \ b₃ <= b₄ holds
b₂ <= b₃ "\/" b₄

proof end;

theorem Th39: :: YELLOW_5:39

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds
( 'not' (b₂ "\/" b₃) = ('not' b₂) "/\" ('not' b₃) & 'not' (b₂ "/\" b₃) = ('not' b₂) "\/" ('not' b₃) )

proof end;

theorem Th40: :: YELLOW_5:40

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
'not' b₃ <= 'not' b₂

proof end;

theorem Th41: :: YELLOW_5:41

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₄ \ b₃ <= b₄ \ b₂

proof end;

theorem Th42: :: YELLOW_5:42

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <= b₃ & b₄ <= b₅ holds
b₂ \ b₅ <= b₃ \ b₄

proof end;

theorem Th43: :: YELLOW_5:43

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ "\/" b₄ holds
( b₂ \ b₃ <= b₄ & b₂ \ b₄ <= b₃ )

proof end;

theorem Th44: :: YELLOW_5:44

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds
( 'not' b₂ <= 'not' (b₂ "/\" b₃) & 'not' b₃ <= 'not' (b₂ "/\" b₃) )

proof end;

theorem Th45: :: YELLOW_5:45

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds
( 'not' (b₂ "\/" b₃) <= 'not' b₂ & 'not' (b₂ "\/" b₃) <= 'not' b₃ )

proof end;

theorem Th46: :: YELLOW_5:46

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ \ b₂ holds
b₂ = Bottom b₁

proof end;

theorem Th47: :: YELLOW_5:47

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
b₃ = b₂ "\/" (b₃ \ b₂)

proof end;

theorem Th48: :: YELLOW_5:48

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ \ b₃ = Bottom b₁ iff b₂ <= b₃ )

proof end;

theorem Th49: :: YELLOW_5:49

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ "\/" b₄ & b₂ "/\" b₄ = Bottom b₁ holds
b₂ <= b₃

proof end;

theorem Th50: :: YELLOW_5:50

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = (b₂ \ b₃) "\/" b₃

proof end;

theorem Th51: :: YELLOW_5:51

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ (b₂ "\/" b₃) = Bottom b₁

proof end;

theorem Th52: :: YELLOW_5:52

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ (b₂ "/\" b₃) = b₂ \ b₃

proof end;

theorem Th53: :: YELLOW_5:53

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds (b₂ \ b₃) "/\" b₃ = Bottom b₁

proof end;

theorem Th54: :: YELLOW_5:54

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ "\/" (b₃ \ b₂) = b₂ "\/" b₃

proof end;

theorem Th55: :: YELLOW_5:55

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds (b₂ "/\" b₃) "\/" (b₂ \ b₃) = b₂

proof end;

theorem Th56: :: YELLOW_5:56

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ \ b₄) = (b₂ \ b₃) "\/" (b₂ "/\" b₄)

proof end;

theorem Th57: :: YELLOW_5:57

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ (b₂ \ b₃) = b₂ "/\" b₃

proof end;

theorem Th58: :: YELLOW_5:58

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) \ b₃ = b₂ \ b₃

proof end;

theorem Th59: :: YELLOW_5:59

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ "/\" b₃ = Bottom b₁ iff b₂ \ b₃ = b₂ )

proof end;

theorem Th60: :: YELLOW_5:60

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ "\/" b₄) = (b₂ \ b₃) "/\" (b₂ \ b₄)

proof end;

theorem Th61: :: YELLOW_5:61

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ \ (b₃ "/\" b₄) = (b₂ \ b₃) "\/" (b₂ \ b₄)

proof end;

theorem Th62: :: YELLOW_5:62

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" (b₃ \ b₄) = (b₂ "/\" b₃) \ (b₂ "/\" b₄)

proof end;

theorem Th63: :: YELLOW_5:63

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) \ (b₂ "/\" b₃) = (b₂ \ b₃) "\/" (b₃ \ b₂)

proof end;

theorem Th64: :: YELLOW_5:64

for b₁ being non empty Boolean RelStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ \ b₃) \ b₄ = b₂ \ (b₃ "\/" b₄)

proof end;

theorem Th65: :: YELLOW_5:65

for b₁ being non empty Boolean RelStr holds 'not' (Bottom b₁) = Top b₁

proof end;

theorem Th66: :: YELLOW_5:66

for b₁ being non empty Boolean RelStr holds 'not' (Top b₁) = Bottom b₁

proof end;

theorem Th67: :: YELLOW_5:67

for b₁ being non empty Boolean RelStr
for b₂ being Element of b₁ holds b₂ \ b₂ = Bottom b₁ by Th37;

theorem Th68: :: YELLOW_5:68

for b₁ being non empty Boolean RelStr
for b₂ being Element of b₁ holds b₂ \ (Bottom b₁) = b₂

proof end;

theorem Th69: :: YELLOW_5:69

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds 'not' (b₂ \ b₃) = ('not' b₂) "\/" b₃

proof end;

theorem Th70: :: YELLOW_5:70

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ misses b₂ \ b₃

proof end;

theorem Th71: :: YELLOW_5:71

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ holds b₂ \ b₃ misses b₃

proof end;

theorem Th72: :: YELLOW_5:72

for b₁ being non empty Boolean RelStr
for b₂, b₃ being Element of b₁ st b₂ misses b₃ holds
(b₂ "\/" b₃) \ b₃ = b₂

proof end;