:: YELLOW_4 semantic presentation

theorem Th1: :: YELLOW_4:1

for b₁ being RelStr
for b₂ being set
for b₃ being Element of b₁ st b₃ in b₂ & ex_sup_of b₂,b₁ holds
b₃ <= "\/" b₂,b₁

proof end;

theorem Th2: :: YELLOW_4:2

for b₁ being RelStr
for b₂ being set
for b₃ being Element of b₁ st b₃ in b₂ & ex_inf_of b₂,b₁ holds
"/\" b₂,b₁ <= b₃

proof end;

definition

let c₁ be RelStr ;
let c₂, c₃ be Subset of c₁;
pred c₂ is_finer_than c₃ means :Def1: :: YELLOW_4:def 1
for b₁ being Element of a₁ st b₁ in a₂ holds
ex b₂ being Element of a₁ st
( b₂ in a₃ & b₁ <= b₂ );
pred c₃ is_coarser_than c₂ means :Def2: :: YELLOW_4:def 2
for b₁ being Element of a₁ st b₁ in a₃ holds
ex b₂ being Element of a₁ st
( b₂ in a₂ & b₂ <= b₁ );

end;

:: deftheorem Def1 defines is_finer_than YELLOW_4:def 1 :

:: deftheorem Def2 defines is_coarser_than YELLOW_4:def 2 :

definition

let c₁ be non empty reflexive RelStr ;
let c₂, c₃ be Subset of c₁;
redefine pred is_finer_than as c₂ is_finer_than c₃;
reflexivity

proof end;

redefine pred is_coarser_than as c₃ is_coarser_than c₂;
reflexivity

proof end;

end;

theorem Th3: :: YELLOW_4:3

for b₁ being RelStr
for b₂ being Subset of b₁ holds {} b₁ is_finer_than b₂

proof end;

theorem Th4: :: YELLOW_4:4

for b₁ being transitive RelStr
for b₂, b₃, b₄ being Subset of b₁ st b₂ is_finer_than b₃ & b₃ is_finer_than b₄ holds
b₂ is_finer_than b₄

proof end;

theorem Th5: :: YELLOW_4:5

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₃ is_finer_than b₂ & b₂ is lower holds
b₃ c= b₂

proof end;

theorem Th6: :: YELLOW_4:6

for b₁ being RelStr
for b₂ being Subset of b₁ holds {} b₁ is_coarser_than b₂

proof end;

theorem Th7: :: YELLOW_4:7

for b₁ being transitive RelStr
for b₂, b₃, b₄ being Subset of b₁ st b₄ is_coarser_than b₃ & b₃ is_coarser_than b₂ holds
b₄ is_coarser_than b₂

proof end;

theorem Th8: :: YELLOW_4:8

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₂ is_coarser_than b₃ & b₃ is upper holds
b₂ c= b₃

proof end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Subset of c₁;
func c₂ "\/" c₃ -> Subset of a₁ equals :: YELLOW_4:def 3
{ (b₁ "\/" b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines "\/" YELLOW_4:def 3 :

definition

let c₁ be antisymmetric with_suprema RelStr ;
let c₂, c₃ be Subset of c₁;
redefine func "\/" as c₂ "\/" c₃ -> Subset of a₁;
commutativity

proof end;

end;

theorem Th9: :: YELLOW_4:9

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds b₂ "\/" ({} b₁) = {}

proof end;

theorem Th10: :: YELLOW_4:10

for b₁ being non empty RelStr
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Element of b₁ st b₄ in b₂ & b₅ in b₃ holds
b₄ "\/" b₅ in b₂ "\/" b₃ ;

theorem Th11: :: YELLOW_4:11

for b₁ being antisymmetric with_suprema RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ is_finer_than b₂ "\/" b₃

proof end;

theorem Th12: :: YELLOW_4:12

for b₁ being antisymmetric with_suprema RelStr
for b₂, b₃ being Subset of b₁ holds b₂ "\/" b₃ is_coarser_than b₂

proof end;

theorem Th13: :: YELLOW_4:13

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

proof end;

theorem Th14: :: YELLOW_4:14

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ "\/" b₃) "\/" b₄ = b₂ "\/" (b₃ "\/" b₄)

proof end;

registration

let c₁ be non empty RelStr ;
let c₂, c₃ be non empty Subset of c₁;
cluster a₂ "\/" a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be transitive antisymmetric with_suprema RelStr ;
let c₂, c₃ be directed Subset of c₁;
cluster a₂ "\/" a₃ -> directed ;
coherence

proof end;

end;

registration

let c₁ be transitive antisymmetric with_suprema RelStr ;
let c₂, c₃ be filtered Subset of c₁;
cluster a₂ "\/" a₃ -> filtered ;
coherence

proof end;

end;

registration

let c₁ be with_suprema Poset;
let c₂, c₃ be upper Subset of c₁;
cluster a₂ "\/" a₃ -> upper ;
coherence

proof end;

end;

theorem Th15: :: YELLOW_4:15

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds {b₃} "\/" b₂ = { (b₃ "\/" b₄) where B is Element of b₁ : b₄ in b₂ }

proof end;

theorem Th16: :: YELLOW_4:16

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

proof end;

theorem Th17: :: YELLOW_4:17

for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Subset of b₁ holds b₂ \/ (b₃ "\/" b₄) c= (b₂ \/ b₃) "\/" (b₂ \/ b₄)

proof end;

theorem Th18: :: YELLOW_4:18

for b₁ being antisymmetric with_suprema RelStr
for b₂ being upper Subset of b₁
for b₃, b₄ being Subset of b₁ holds (b₂ \/ b₃) "\/" (b₂ \/ b₄) c= b₂ \/ (b₃ "\/" b₄)

proof end;

E6: now

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
thus { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } = {(c₂ "\/" c₃)}

proof

thus { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } c= {(c₂ "\/" c₃)} :: according to XBOOLE_0:def 10

proof

let c₄ be set ; :: according to TARSKI:def 3
assume c₄ in { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } ;
then consider c₅, c₆ being Element of c₁ such that
E7: c₄ = c₅ "\/" c₆ and
E8: ( c₅ in {c₂} & c₆ in {c₃} ) ;
( c₅ = c₂ & c₆ = c₃ ) by E8, TARSKI:def 1;
hence c₄ in {(c₂ "\/" c₃)} by E7, TARSKI:def 1;

end;

let c₄ be set ; :: according to TARSKI:def 3
assume c₄ in {(c₂ "\/" c₃)} ;
then ( c₄ = c₂ "\/" c₃ & c₂ in {c₂} & c₃ in {c₃} ) by TARSKI:def 1;
hence c₄ in { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } ;

end;

E7: now

let c₁ be non empty RelStr ;
let c₂, c₃, c₄ be Element of c₁;
thus { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } = {(c₂ "\/" c₃),(c₂ "\/" c₄)}

proof

thus { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } c= {(c₂ "\/" c₃),(c₂ "\/" c₄)} :: according to XBOOLE_0:def 10

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } ;
then consider c₆, c₇ being Element of c₁ such that
E8: c₅ = c₆ "\/" c₇ and
E9: ( c₆ in {c₂} & c₇ in {c₃,c₄} ) ;
( c₆ = c₂ & ( c₇ = c₃ or c₇ = c₄ ) ) by E9, TARSKI:def 1, TARSKI:def 2;
hence c₅ in {(c₂ "\/" c₃),(c₂ "\/" c₄)} by E8, TARSKI:def 2;

end;

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in {(c₂ "\/" c₃),(c₂ "\/" c₄)} ;
then E8: ( c₅ = c₂ "\/" c₃ or c₅ = c₂ "\/" c₄ ) by TARSKI:def 2;
( c₂ in {c₂} & c₃ in {c₃,c₄} & c₄ in {c₃,c₄} ) by TARSKI:def 1, TARSKI:def 2;
hence c₅ in { (b₁ "\/" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } by E8;

end;

theorem Th19: :: YELLOW_4:19

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds {b₂} "\/" {b₃} = {(b₂ "\/" b₃)} by Lemma6;

theorem Th20: :: YELLOW_4:20

for b₁ being non empty RelStr
for b₂, b₃, b₄ being Element of b₁ holds {b₂} "\/" {b₃,b₄} = {(b₂ "\/" b₃),(b₂ "\/" b₄)} by Lemma7;

theorem Th21: :: YELLOW_4:21

for b₁ being non empty RelStr
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₄ & b₃ c= b₅ holds
b₂ "\/" b₃ c= b₄ "\/" b₅

proof end;

theorem Th22: :: YELLOW_4:22

for b₁ being reflexive antisymmetric with_suprema RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ is_<=_than b₂ holds
{b₃} "\/" b₂ = b₂

proof end;

theorem Th23: :: YELLOW_4:23

for b₁ being antisymmetric with_suprema RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₃ is_<=_than {b₃} "\/" b₂

proof end;

theorem Th24: :: YELLOW_4:24

for b₁ being with_suprema Poset
for b₂ being Subset of b₁
for b₃ being Element of b₁ st ex_inf_of {b₃} "\/" b₂,b₁ & ex_inf_of b₂,b₁ holds
b₃ "\/" (inf b₂) <= inf ({b₃} "\/" b₂)

proof end;

theorem Th25: :: YELLOW_4:25

for b₁ being non empty transitive antisymmetric complete RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ is_<=_than sup (b₂ "\/" b₃)

proof end;

theorem Th26: :: YELLOW_4:26

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

proof end;

theorem Th27: :: YELLOW_4:27

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂ is_>=_than b₄ & b₃ is_>=_than b₅ holds
b₂ "\/" b₃ is_>=_than b₄ "\/" b₅

proof end;

theorem Th28: :: YELLOW_4:28

for b₁ being non empty complete Poset
for b₂, b₃ being non empty Subset of b₁ holds sup (b₂ "\/" b₃) = (sup b₂) "\/" (sup b₃)

proof end;

theorem Th29: :: YELLOW_4:29

for b₁ being antisymmetric with_suprema RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ c= downarrow (b₂ "\/" b₃)

proof end;

theorem Th30: :: YELLOW_4:30

for b₁ being with_suprema Poset
for b₂, b₃ being Element of (InclPoset (Ids b₁))
for b₄, b₅ being Subset of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "\/" b₃ = downarrow (b₄ "\/" b₅)

proof end;

theorem Th31: :: YELLOW_4:31

for b₁ being non empty RelStr
for b₂ being Subset of [:b₁,b₁:] holds union { b₃ where B is Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "\/" (proj2 b₂) & b₄ in proj1 b₂ ) } = (proj1 b₂) "\/" (proj2 b₂)

proof end;

theorem Th32: :: YELLOW_4:32

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃ being Subset of b₁ holds downarrow ((downarrow b₂) "\/" (downarrow b₃)) c= downarrow (b₂ "\/" b₃)

proof end;

theorem Th33: :: YELLOW_4:33

for b₁ being with_suprema Poset
for b₂, b₃ being Subset of b₁ holds downarrow ((downarrow b₂) "\/" (downarrow b₃)) = downarrow (b₂ "\/" b₃)

proof end;

theorem Th34: :: YELLOW_4:34

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃ being Subset of b₁ holds uparrow ((uparrow b₂) "\/" (uparrow b₃)) c= uparrow (b₂ "\/" b₃)

proof end;

theorem Th35: :: YELLOW_4:35

for b₁ being with_suprema Poset
for b₂, b₃ being Subset of b₁ holds uparrow ((uparrow b₂) "\/" (uparrow b₃)) = uparrow (b₂ "\/" b₃)

proof end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Subset of c₁;
func c₂ "/\" c₃ -> Subset of a₁ equals :: YELLOW_4:def 4
{ (b₁ "/\" b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def4 defines "/\" YELLOW_4:def 4 :

definition

let c₁ be antisymmetric with_infima RelStr ;
let c₂, c₃ be Subset of c₁;
redefine func "/\" as c₂ "/\" c₃ -> Subset of a₁;
commutativity

proof end;

end;

theorem Th36: :: YELLOW_4:36

for b₁ being non empty RelStr
for b₂ being Subset of b₁ holds b₂ "/\" ({} b₁) = {}

proof end;

theorem Th37: :: YELLOW_4:37

for b₁ being non empty RelStr
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Element of b₁ st b₄ in b₂ & b₅ in b₃ holds
b₄ "/\" b₅ in b₂ "/\" b₃ ;

theorem Th38: :: YELLOW_4:38

for b₁ being antisymmetric with_infima RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ is_coarser_than b₂ "/\" b₃

proof end;

theorem Th39: :: YELLOW_4:39

for b₁ being antisymmetric with_infima RelStr
for b₂, b₃ being Subset of b₁ holds b₂ "/\" b₃ is_finer_than b₂

proof end;

theorem Th40: :: YELLOW_4:40

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

proof end;

theorem Th41: :: YELLOW_4:41

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ "/\" b₃) "/\" b₄ = b₂ "/\" (b₃ "/\" b₄)

proof end;

registration

let c₁ be non empty RelStr ;
let c₂, c₃ be non empty Subset of c₁;
cluster a₂ "/\" a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be transitive antisymmetric with_infima RelStr ;
let c₂, c₃ be directed Subset of c₁;
cluster a₂ "/\" a₃ -> directed ;
coherence

proof end;

end;

registration

let c₁ be transitive antisymmetric with_infima RelStr ;
let c₂, c₃ be filtered Subset of c₁;
cluster a₂ "/\" a₃ -> filtered ;
coherence

proof end;

end;

registration

let c₁ be Semilattice;
let c₂, c₃ be lower Subset of c₁;
cluster a₂ "/\" a₃ -> lower ;
coherence

proof end;

end;

theorem Th42: :: YELLOW_4:42

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds {b₃} "/\" b₂ = { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ }

proof end;

theorem Th43: :: YELLOW_4:43

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

proof end;

theorem Th44: :: YELLOW_4:44

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Subset of b₁ holds b₂ \/ (b₃ "/\" b₄) c= (b₂ \/ b₃) "/\" (b₂ \/ b₄)

proof end;

theorem Th45: :: YELLOW_4:45

for b₁ being antisymmetric with_infima RelStr
for b₂ being lower Subset of b₁
for b₃, b₄ being Subset of b₁ holds (b₂ \/ b₃) "/\" (b₂ \/ b₄) c= b₂ \/ (b₃ "/\" b₄)

proof end;

E14: now

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
thus { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } = {(c₂ "/\" c₃)}

proof

thus { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } c= {(c₂ "/\" c₃)} :: according to XBOOLE_0:def 10

proof

let c₄ be set ; :: according to TARSKI:def 3
assume c₄ in { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } ;
then consider c₅, c₆ being Element of c₁ such that
E15: c₄ = c₅ "/\" c₆ and
E16: ( c₅ in {c₂} & c₆ in {c₃} ) ;
( c₅ = c₂ & c₆ = c₃ ) by E16, TARSKI:def 1;
hence c₄ in {(c₂ "/\" c₃)} by E15, TARSKI:def 1;

end;

let c₄ be set ; :: according to TARSKI:def 3
assume c₄ in {(c₂ "/\" c₃)} ;
then ( c₄ = c₂ "/\" c₃ & c₂ in {c₂} & c₃ in {c₃} ) by TARSKI:def 1;
hence c₄ in { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃} ) } ;

end;

E15: now

let c₁ be non empty RelStr ;
let c₂, c₃, c₄ be Element of c₁;
thus { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } = {(c₂ "/\" c₃),(c₂ "/\" c₄)}

proof

thus { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } c= {(c₂ "/\" c₃),(c₂ "/\" c₄)} :: according to XBOOLE_0:def 10

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } ;
then consider c₆, c₇ being Element of c₁ such that
E16: c₅ = c₆ "/\" c₇ and
E17: ( c₆ in {c₂} & c₇ in {c₃,c₄} ) ;
( c₆ = c₂ & ( c₇ = c₃ or c₇ = c₄ ) ) by E17, TARSKI:def 1, TARSKI:def 2;
hence c₅ in {(c₂ "/\" c₃),(c₂ "/\" c₄)} by E16, TARSKI:def 2;

end;

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in {(c₂ "/\" c₃),(c₂ "/\" c₄)} ;
then E16: ( c₅ = c₂ "/\" c₃ or c₅ = c₂ "/\" c₄ ) by TARSKI:def 2;
( c₂ in {c₂} & c₃ in {c₃,c₄} & c₄ in {c₃,c₄} ) by TARSKI:def 1, TARSKI:def 2;
hence c₅ in { (b₁ "/\" b₂) where B is Element of c₁, B is Element of c₁ : ( b₁ in {c₂} & b₂ in {c₃,c₄} ) } by E16;

end;

theorem Th46: :: YELLOW_4:46

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds {b₂} "/\" {b₃} = {(b₂ "/\" b₃)} by Lemma14;

theorem Th47: :: YELLOW_4:47

for b₁ being non empty RelStr
for b₂, b₃, b₄ being Element of b₁ holds {b₂} "/\" {b₃,b₄} = {(b₂ "/\" b₃),(b₂ "/\" b₄)} by Lemma15;

theorem Th48: :: YELLOW_4:48

for b₁ being non empty RelStr
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ c= b₄ & b₃ c= b₅ holds
b₂ "/\" b₃ c= b₄ "/\" b₅

proof end;

theorem Th49: :: YELLOW_4:49

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂, b₃ being Subset of b₁ holds b₂ /\ b₃ c= b₂ "/\" b₃

proof end;

theorem Th50: :: YELLOW_4:50

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂, b₃ being lower Subset of b₁ holds b₂ "/\" b₃ = b₂ /\ b₃

proof end;

theorem Th51: :: YELLOW_4:51

for b₁ being reflexive antisymmetric with_infima RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ is_>=_than b₂ holds
{b₃} "/\" b₂ = b₂

proof end;

theorem Th52: :: YELLOW_4:52

for b₁ being antisymmetric with_infima RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds {b₃} "/\" b₂ is_<=_than b₃

proof end;

theorem Th53: :: YELLOW_4:53

for b₁ being Semilattice
for b₂ being Subset of b₁
for b₃ being Element of b₁ st ex_sup_of {b₃} "/\" b₂,b₁ & ex_sup_of b₂,b₁ holds
sup ({b₃} "/\" b₂) <= b₃ "/\" (sup b₂)

proof end;

theorem Th54: :: YELLOW_4:54

for b₁ being non empty transitive antisymmetric complete RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ is_>=_than inf (b₂ "/\" b₃)

proof end;

theorem Th55: :: YELLOW_4:55

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

proof end;

theorem Th56: :: YELLOW_4:56

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃ being Element of b₁
for b₄, b₅ being Subset of b₁ st b₂ is_>=_than b₄ & b₃ is_>=_than b₅ holds
b₂ "/\" b₃ is_>=_than b₄ "/\" b₅

proof end;

theorem Th57: :: YELLOW_4:57

for b₁ being non empty complete Poset
for b₂, b₃ being non empty Subset of b₁ holds inf (b₂ "/\" b₃) = (inf b₂) "/\" (inf b₃)

proof end;

theorem Th58: :: YELLOW_4:58

for b₁ being Semilattice
for b₂, b₃ being Element of (InclPoset (Ids b₁))
for b₄, b₅ being Subset of b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ "/\" b₃ = b₄ "/\" b₅

proof end;

theorem Th59: :: YELLOW_4:59

for b₁ being antisymmetric with_infima RelStr
for b₂ being Subset of b₁
for b₃ being non empty Subset of b₁ holds b₂ c= uparrow (b₂ "/\" b₃)

proof end;

theorem Th60: :: YELLOW_4:60

for b₁ being non empty RelStr
for b₂ being Subset of [:b₁,b₁:] holds union { b₃ where B is Subset of b₁ : ex b₁ being Element of b₁ st
( b₃ = {b₄} "/\" (proj2 b₂) & b₄ in proj1 b₂ ) } = (proj1 b₂) "/\" (proj2 b₂)

proof end;

theorem Th61: :: YELLOW_4:61

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃ being Subset of b₁ holds downarrow ((downarrow b₂) "/\" (downarrow b₃)) c= downarrow (b₂ "/\" b₃)

proof end;

theorem Th62: :: YELLOW_4:62

for b₁ being Semilattice
for b₂, b₃ being Subset of b₁ holds downarrow ((downarrow b₂) "/\" (downarrow b₃)) = downarrow (b₂ "/\" b₃)

proof end;

theorem Th63: :: YELLOW_4:63

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃ being Subset of b₁ holds uparrow ((uparrow b₂) "/\" (uparrow b₃)) c= uparrow (b₂ "/\" b₃)

proof end;

theorem Th64: :: YELLOW_4:64

for b₁ being Semilattice
for b₂, b₃ being Subset of b₁ holds uparrow ((uparrow b₂) "/\" (uparrow b₃)) = uparrow (b₂ "/\" b₃)

proof end;