:: YELLOW_4 semantic presentation

theorem Th1: :: YELLOW_4:1
for b1 being RelStr
for b2 being set
for b3 being Element of b1 st b3 in b2 & ex_sup_of b2,b1 holds
b3 <= "\/" b2,b1
proof end;

theorem Th2: :: YELLOW_4:2
for b1 being RelStr
for b2 being set
for b3 being Element of b1 st b3 in b2 & ex_inf_of b2,b1 holds
"/\" b2,b1 <= b3
proof end;

definition
let c1 be RelStr ;
let c2, c3 be Subset of c1;
pred c2 is_finer_than c3 means :Def1: :: YELLOW_4:def 1
for b1 being Element of a1 st b1 in a2 holds
ex b2 being Element of a1 st
( b2 in a3 & b1 <= b2 );
pred c3 is_coarser_than c2 means :Def2: :: YELLOW_4:def 2
for b1 being Element of a1 st b1 in a3 holds
ex b2 being Element of a1 st
( b2 in a2 & b2 <= b1 );
end;

:: deftheorem Def1 defines is_finer_than YELLOW_4:def 1 :
for b1 being RelStr
for b2, b3 being Subset of b1 holds
( b2 is_finer_than b3 iff for b4 being Element of b1 st b4 in b2 holds
ex b5 being Element of b1 st
( b5 in b3 & b4 <= b5 ) );

:: deftheorem Def2 defines is_coarser_than YELLOW_4:def 2 :
for b1 being RelStr
for b2, b3 being Subset of b1 holds
( b3 is_coarser_than b2 iff for b4 being Element of b1 st b4 in b3 holds
ex b5 being Element of b1 st
( b5 in b2 & b5 <= b4 ) );

definition
let c1 be non empty reflexive RelStr ;
let c2, c3 be Subset of c1;
redefine pred is_finer_than as c2 is_finer_than c3;
reflexivity
for b1 being Subset of c1 holds b1 is_finer_than b1
proof end;
redefine pred is_coarser_than as c3 is_coarser_than c2;
reflexivity
for b1 being Subset of c1 holds b1 is_coarser_than b1
proof end;
end;

theorem Th3: :: YELLOW_4:3
for b1 being RelStr
for b2 being Subset of b1 holds {} b1 is_finer_than b2
proof end;

theorem Th4: :: YELLOW_4:4
for b1 being transitive RelStr
for b2, b3, b4 being Subset of b1 st b2 is_finer_than b3 & b3 is_finer_than b4 holds
b2 is_finer_than b4
proof end;

theorem Th5: :: YELLOW_4:5
for b1 being RelStr
for b2, b3 being Subset of b1 st b3 is_finer_than b2 & b2 is lower holds
b3 c= b2
proof end;

theorem Th6: :: YELLOW_4:6
for b1 being RelStr
for b2 being Subset of b1 holds {} b1 is_coarser_than b2
proof end;

theorem Th7: :: YELLOW_4:7
for b1 being transitive RelStr
for b2, b3, b4 being Subset of b1 st b4 is_coarser_than b3 & b3 is_coarser_than b2 holds
b4 is_coarser_than b2
proof end;

theorem Th8: :: YELLOW_4:8
for b1 being RelStr
for b2, b3 being Subset of b1 st b2 is_coarser_than b3 & b3 is upper holds
b2 c= b3
proof end;

definition
let c1 be non empty RelStr ;
let c2, c3 be Subset of c1;
func c2 "\/" c3 -> Subset of a1 equals :: YELLOW_4:def 3
{ (b1 "\/" b2) where B is Element of a1, B is Element of a1 : ( b1 in a2 & b2 in a3 ) } ;
coherence
{ (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in c2 & b2 in c3 ) } is Subset of c1
proof end;
end;

:: deftheorem Def3 defines "\/" YELLOW_4:def 3 :
for b1 being non empty RelStr
for b2, b3 being Subset of b1 holds b2 "\/" b3 = { (b4 "\/" b5) where B is Element of b1, B is Element of b1 : ( b4 in b2 & b5 in b3 ) } ;

definition
let c1 be antisymmetric with_suprema RelStr ;
let c2, c3 be Subset of c1;
redefine func "\/" as c2 "\/" c3 -> Subset of a1;
commutativity
for b1, b2 being Subset of c1 holds b1 "\/" b2 = b2 "\/" b1
proof end;
end;

theorem Th9: :: YELLOW_4:9
for b1 being non empty RelStr
for b2 being Subset of b1 holds b2 "\/" ({} b1) = {}
proof end;

theorem Th10: :: YELLOW_4:10
for b1 being non empty RelStr
for b2, b3 being Subset of b1
for b4, b5 being Element of b1 st b4 in b2 & b5 in b3 holds
b4 "\/" b5 in b2 "\/" b3 ;

theorem Th11: :: YELLOW_4:11
for b1 being antisymmetric with_suprema RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 is_finer_than b2 "\/" b3
proof end;

theorem Th12: :: YELLOW_4:12
for b1 being antisymmetric with_suprema RelStr
for b2, b3 being Subset of b1 holds b2 "\/" b3 is_coarser_than b2
proof end;

theorem Th13: :: YELLOW_4:13
for b1 being reflexive antisymmetric with_suprema RelStr
for b2 being Subset of b1 holds b2 c= b2 "\/" b2
proof end;

theorem Th14: :: YELLOW_4:14
for b1 being transitive antisymmetric with_suprema RelStr
for b2, b3, b4 being Subset of b1 holds (b2 "\/" b3) "\/" b4 = b2 "\/" (b3 "\/" b4)
proof end;

registration
let c1 be non empty RelStr ;
let c2, c3 be non empty Subset of c1;
cluster a2 "\/" a3 -> non empty ;
coherence
not c2 "\/" c3 is empty
proof end;
end;

registration
let c1 be transitive antisymmetric with_suprema RelStr ;
let c2, c3 be directed Subset of c1;
cluster a2 "\/" a3 -> directed ;
coherence
c2 "\/" c3 is directed
proof end;
end;

registration
let c1 be transitive antisymmetric with_suprema RelStr ;
let c2, c3 be filtered Subset of c1;
cluster a2 "\/" a3 -> filtered ;
coherence
c2 "\/" c3 is filtered
proof end;
end;

registration
let c1 be with_suprema Poset;
let c2, c3 be upper Subset of c1;
cluster a2 "\/" a3 -> upper ;
coherence
c2 "\/" c3 is upper
proof end;
end;

theorem Th15: :: YELLOW_4:15
for b1 being non empty RelStr
for b2 being Subset of b1
for b3 being Element of b1 holds {b3} "\/" b2 = { (b3 "\/" b4) where B is Element of b1 : b4 in b2 }
proof end;

theorem Th16: :: YELLOW_4:16
for b1 being non empty RelStr
for b2, b3, b4 being Subset of b1 holds b2 "\/" (b3 \/ b4) = (b2 "\/" b3) \/ (b2 "\/" b4)
proof end;

theorem Th17: :: YELLOW_4:17
for b1 being reflexive antisymmetric with_suprema RelStr
for b2, b3, b4 being Subset of b1 holds b2 \/ (b3 "\/" b4) c= (b2 \/ b3) "\/" (b2 \/ b4)
proof end;

theorem Th18: :: YELLOW_4:18
for b1 being antisymmetric with_suprema RelStr
for b2 being upper Subset of b1
for b3, b4 being Subset of b1 holds (b2 \/ b3) "\/" (b2 \/ b4) c= b2 \/ (b3 "\/" b4)
proof end;

E6: now
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
thus { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } = {(c2 "\/" c3)}
proof
thus { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } c= {(c2 "\/" c3)} :: according to XBOOLE_0:def 10
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } ;
then consider c5, c6 being Element of c1 such that
E7: c4 = c5 "\/" c6 and
E8: ( c5 in {c2} & c6 in {c3} ) ;
( c5 = c2 & c6 = c3 ) by E8, TARSKI:def 1;
hence c4 in {(c2 "\/" c3)} by E7, TARSKI:def 1;
end;
let c4 be set ; :: according to TARSKI:def 3
assume c4 in {(c2 "\/" c3)} ;
then ( c4 = c2 "\/" c3 & c2 in {c2} & c3 in {c3} ) by TARSKI:def 1;
hence c4 in { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } ;
end;
end;

E7: now
let c1 be non empty RelStr ;
let c2, c3, c4 be Element of c1;
thus { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } = {(c2 "\/" c3),(c2 "\/" c4)}
proof
thus { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } c= {(c2 "\/" c3),(c2 "\/" c4)} :: according to XBOOLE_0:def 10
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } ;
then consider c6, c7 being Element of c1 such that
E8: c5 = c6 "\/" c7 and
E9: ( c6 in {c2} & c7 in {c3,c4} ) ;
( c6 = c2 & ( c7 = c3 or c7 = c4 ) ) by E9, TARSKI:def 1, TARSKI:def 2;
hence c5 in {(c2 "\/" c3),(c2 "\/" c4)} by E8, TARSKI:def 2;
end;
let c5 be set ; :: according to TARSKI:def 3
assume c5 in {(c2 "\/" c3),(c2 "\/" c4)} ;
then E8: ( c5 = c2 "\/" c3 or c5 = c2 "\/" c4 ) by TARSKI:def 2;
( c2 in {c2} & c3 in {c3,c4} & c4 in {c3,c4} ) by TARSKI:def 1, TARSKI:def 2;
hence c5 in { (b1 "\/" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } by E8;
end;
end;

theorem Th19: :: YELLOW_4:19
for b1 being non empty RelStr
for b2, b3 being Element of b1 holds {b2} "\/" {b3} = {(b2 "\/" b3)} by Lemma6;

theorem Th20: :: YELLOW_4:20
for b1 being non empty RelStr
for b2, b3, b4 being Element of b1 holds {b2} "\/" {b3,b4} = {(b2 "\/" b3),(b2 "\/" b4)} by Lemma7;

theorem Th21: :: YELLOW_4:21
for b1 being non empty RelStr
for b2, b3, b4, b5 being Subset of b1 st b2 c= b4 & b3 c= b5 holds
b2 "\/" b3 c= b4 "\/" b5
proof end;

theorem Th22: :: YELLOW_4:22
for b1 being reflexive antisymmetric with_suprema RelStr
for b2 being Subset of b1
for b3 being Element of b1 st b3 is_<=_than b2 holds
{b3} "\/" b2 = b2
proof end;

theorem Th23: :: YELLOW_4:23
for b1 being antisymmetric with_suprema RelStr
for b2 being Subset of b1
for b3 being Element of b1 holds b3 is_<=_than {b3} "\/" b2
proof end;

theorem Th24: :: YELLOW_4:24
for b1 being with_suprema Poset
for b2 being Subset of b1
for b3 being Element of b1 st ex_inf_of {b3} "\/" b2,b1 & ex_inf_of b2,b1 holds
b3 "\/" (inf b2) <= inf ({b3} "\/" b2)
proof end;

theorem Th25: :: YELLOW_4:25
for b1 being non empty transitive antisymmetric complete RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 is_<=_than sup (b2 "\/" b3)
proof end;

theorem Th26: :: YELLOW_4:26
for b1 being transitive antisymmetric with_suprema RelStr
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b2 is_<=_than b4 & b3 is_<=_than b5 holds
b2 "\/" b3 is_<=_than b4 "\/" b5
proof end;

theorem Th27: :: YELLOW_4:27
for b1 being transitive antisymmetric with_suprema RelStr
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b2 is_>=_than b4 & b3 is_>=_than b5 holds
b2 "\/" b3 is_>=_than b4 "\/" b5
proof end;

theorem Th28: :: YELLOW_4:28
for b1 being non empty complete Poset
for b2, b3 being non empty Subset of b1 holds sup (b2 "\/" b3) = (sup b2) "\/" (sup b3)
proof end;

theorem Th29: :: YELLOW_4:29
for b1 being antisymmetric with_suprema RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 c= downarrow (b2 "\/" b3)
proof end;

theorem Th30: :: YELLOW_4:30
for b1 being with_suprema Poset
for b2, b3 being Element of (InclPoset (Ids b1))
for b4, b5 being Subset of b1 st b2 = b4 & b3 = b5 holds
b2 "\/" b3 = downarrow (b4 "\/" b5)
proof end;

theorem Th31: :: YELLOW_4:31
for b1 being non empty RelStr
for b2 being Subset of [:b1,b1:] holds union { b3 where B is Subset of b1 : ex b1 being Element of b1 st
( b3 = {b4} "\/" (proj2 b2) & b4 in proj1 b2 )
}
= (proj1 b2) "\/" (proj2 b2)
proof end;

theorem Th32: :: YELLOW_4:32
for b1 being transitive antisymmetric with_suprema RelStr
for b2, b3 being Subset of b1 holds downarrow ((downarrow b2) "\/" (downarrow b3)) c= downarrow (b2 "\/" b3)
proof end;

theorem Th33: :: YELLOW_4:33
for b1 being with_suprema Poset
for b2, b3 being Subset of b1 holds downarrow ((downarrow b2) "\/" (downarrow b3)) = downarrow (b2 "\/" b3)
proof end;

theorem Th34: :: YELLOW_4:34
for b1 being transitive antisymmetric with_suprema RelStr
for b2, b3 being Subset of b1 holds uparrow ((uparrow b2) "\/" (uparrow b3)) c= uparrow (b2 "\/" b3)
proof end;

theorem Th35: :: YELLOW_4:35
for b1 being with_suprema Poset
for b2, b3 being Subset of b1 holds uparrow ((uparrow b2) "\/" (uparrow b3)) = uparrow (b2 "\/" b3)
proof end;

definition
let c1 be non empty RelStr ;
let c2, c3 be Subset of c1;
func c2 "/\" c3 -> Subset of a1 equals :: YELLOW_4:def 4
{ (b1 "/\" b2) where B is Element of a1, B is Element of a1 : ( b1 in a2 & b2 in a3 ) } ;
coherence
{ (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in c2 & b2 in c3 ) } is Subset of c1
proof end;
end;

:: deftheorem Def4 defines "/\" YELLOW_4:def 4 :
for b1 being non empty RelStr
for b2, b3 being Subset of b1 holds b2 "/\" b3 = { (b4 "/\" b5) where B is Element of b1, B is Element of b1 : ( b4 in b2 & b5 in b3 ) } ;

definition
let c1 be antisymmetric with_infima RelStr ;
let c2, c3 be Subset of c1;
redefine func "/\" as c2 "/\" c3 -> Subset of a1;
commutativity
for b1, b2 being Subset of c1 holds b1 "/\" b2 = b2 "/\" b1
proof end;
end;

theorem Th36: :: YELLOW_4:36
for b1 being non empty RelStr
for b2 being Subset of b1 holds b2 "/\" ({} b1) = {}
proof end;

theorem Th37: :: YELLOW_4:37
for b1 being non empty RelStr
for b2, b3 being Subset of b1
for b4, b5 being Element of b1 st b4 in b2 & b5 in b3 holds
b4 "/\" b5 in b2 "/\" b3 ;

theorem Th38: :: YELLOW_4:38
for b1 being antisymmetric with_infima RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 is_coarser_than b2 "/\" b3
proof end;

theorem Th39: :: YELLOW_4:39
for b1 being antisymmetric with_infima RelStr
for b2, b3 being Subset of b1 holds b2 "/\" b3 is_finer_than b2
proof end;

theorem Th40: :: YELLOW_4:40
for b1 being reflexive antisymmetric with_infima RelStr
for b2 being Subset of b1 holds b2 c= b2 "/\" b2
proof end;

theorem Th41: :: YELLOW_4:41
for b1 being transitive antisymmetric with_infima RelStr
for b2, b3, b4 being Subset of b1 holds (b2 "/\" b3) "/\" b4 = b2 "/\" (b3 "/\" b4)
proof end;

registration
let c1 be non empty RelStr ;
let c2, c3 be non empty Subset of c1;
cluster a2 "/\" a3 -> non empty ;
coherence
not c2 "/\" c3 is empty
proof end;
end;

registration
let c1 be transitive antisymmetric with_infima RelStr ;
let c2, c3 be directed Subset of c1;
cluster a2 "/\" a3 -> directed ;
coherence
c2 "/\" c3 is directed
proof end;
end;

registration
let c1 be transitive antisymmetric with_infima RelStr ;
let c2, c3 be filtered Subset of c1;
cluster a2 "/\" a3 -> filtered ;
coherence
c2 "/\" c3 is filtered
proof end;
end;

registration
let c1 be Semilattice;
let c2, c3 be lower Subset of c1;
cluster a2 "/\" a3 -> lower ;
coherence
c2 "/\" c3 is lower
proof end;
end;

theorem Th42: :: YELLOW_4:42
for b1 being non empty RelStr
for b2 being Subset of b1
for b3 being Element of b1 holds {b3} "/\" b2 = { (b3 "/\" b4) where B is Element of b1 : b4 in b2 }
proof end;

theorem Th43: :: YELLOW_4:43
for b1 being non empty RelStr
for b2, b3, b4 being Subset of b1 holds b2 "/\" (b3 \/ b4) = (b2 "/\" b3) \/ (b2 "/\" b4)
proof end;

theorem Th44: :: YELLOW_4:44
for b1 being reflexive antisymmetric with_infima RelStr
for b2, b3, b4 being Subset of b1 holds b2 \/ (b3 "/\" b4) c= (b2 \/ b3) "/\" (b2 \/ b4)
proof end;

theorem Th45: :: YELLOW_4:45
for b1 being antisymmetric with_infima RelStr
for b2 being lower Subset of b1
for b3, b4 being Subset of b1 holds (b2 \/ b3) "/\" (b2 \/ b4) c= b2 \/ (b3 "/\" b4)
proof end;

E14: now
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
thus { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } = {(c2 "/\" c3)}
proof
thus { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } c= {(c2 "/\" c3)} :: according to XBOOLE_0:def 10
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } ;
then consider c5, c6 being Element of c1 such that
E15: c4 = c5 "/\" c6 and
E16: ( c5 in {c2} & c6 in {c3} ) ;
( c5 = c2 & c6 = c3 ) by E16, TARSKI:def 1;
hence c4 in {(c2 "/\" c3)} by E15, TARSKI:def 1;
end;
let c4 be set ; :: according to TARSKI:def 3
assume c4 in {(c2 "/\" c3)} ;
then ( c4 = c2 "/\" c3 & c2 in {c2} & c3 in {c3} ) by TARSKI:def 1;
hence c4 in { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3} ) } ;
end;
end;

E15: now
let c1 be non empty RelStr ;
let c2, c3, c4 be Element of c1;
thus { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } = {(c2 "/\" c3),(c2 "/\" c4)}
proof
thus { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } c= {(c2 "/\" c3),(c2 "/\" c4)} :: according to XBOOLE_0:def 10
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } ;
then consider c6, c7 being Element of c1 such that
E16: c5 = c6 "/\" c7 and
E17: ( c6 in {c2} & c7 in {c3,c4} ) ;
( c6 = c2 & ( c7 = c3 or c7 = c4 ) ) by E17, TARSKI:def 1, TARSKI:def 2;
hence c5 in {(c2 "/\" c3),(c2 "/\" c4)} by E16, TARSKI:def 2;
end;
let c5 be set ; :: according to TARSKI:def 3
assume c5 in {(c2 "/\" c3),(c2 "/\" c4)} ;
then E16: ( c5 = c2 "/\" c3 or c5 = c2 "/\" c4 ) by TARSKI:def 2;
( c2 in {c2} & c3 in {c3,c4} & c4 in {c3,c4} ) by TARSKI:def 1, TARSKI:def 2;
hence c5 in { (b1 "/\" b2) where B is Element of c1, B is Element of c1 : ( b1 in {c2} & b2 in {c3,c4} ) } by E16;
end;
end;

theorem Th46: :: YELLOW_4:46
for b1 being non empty RelStr
for b2, b3 being Element of b1 holds {b2} "/\" {b3} = {(b2 "/\" b3)} by Lemma14;

theorem Th47: :: YELLOW_4:47
for b1 being non empty RelStr
for b2, b3, b4 being Element of b1 holds {b2} "/\" {b3,b4} = {(b2 "/\" b3),(b2 "/\" b4)} by Lemma15;

theorem Th48: :: YELLOW_4:48
for b1 being non empty RelStr
for b2, b3, b4, b5 being Subset of b1 st b2 c= b4 & b3 c= b5 holds
b2 "/\" b3 c= b4 "/\" b5
proof end;

theorem Th49: :: YELLOW_4:49
for b1 being reflexive antisymmetric with_infima RelStr
for b2, b3 being Subset of b1 holds b2 /\ b3 c= b2 "/\" b3
proof end;

theorem Th50: :: YELLOW_4:50
for b1 being reflexive antisymmetric with_infima RelStr
for b2, b3 being lower Subset of b1 holds b2 "/\" b3 = b2 /\ b3
proof end;

theorem Th51: :: YELLOW_4:51
for b1 being reflexive antisymmetric with_infima RelStr
for b2 being Subset of b1
for b3 being Element of b1 st b3 is_>=_than b2 holds
{b3} "/\" b2 = b2
proof end;

theorem Th52: :: YELLOW_4:52
for b1 being antisymmetric with_infima RelStr
for b2 being Subset of b1
for b3 being Element of b1 holds {b3} "/\" b2 is_<=_than b3
proof end;

theorem Th53: :: YELLOW_4:53
for b1 being Semilattice
for b2 being Subset of b1
for b3 being Element of b1 st ex_sup_of {b3} "/\" b2,b1 & ex_sup_of b2,b1 holds
sup ({b3} "/\" b2) <= b3 "/\" (sup b2)
proof end;

theorem Th54: :: YELLOW_4:54
for b1 being non empty transitive antisymmetric complete RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 is_>=_than inf (b2 "/\" b3)
proof end;

theorem Th55: :: YELLOW_4:55
for b1 being transitive antisymmetric with_infima RelStr
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b2 is_<=_than b4 & b3 is_<=_than b5 holds
b2 "/\" b3 is_<=_than b4 "/\" b5
proof end;

theorem Th56: :: YELLOW_4:56
for b1 being transitive antisymmetric with_infima RelStr
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 st b2 is_>=_than b4 & b3 is_>=_than b5 holds
b2 "/\" b3 is_>=_than b4 "/\" b5
proof end;

theorem Th57: :: YELLOW_4:57
for b1 being non empty complete Poset
for b2, b3 being non empty Subset of b1 holds inf (b2 "/\" b3) = (inf b2) "/\" (inf b3)
proof end;

theorem Th58: :: YELLOW_4:58
for b1 being Semilattice
for b2, b3 being Element of (InclPoset (Ids b1))
for b4, b5 being Subset of b1 st b2 = b4 & b3 = b5 holds
b2 "/\" b3 = b4 "/\" b5
proof end;

theorem Th59: :: YELLOW_4:59
for b1 being antisymmetric with_infima RelStr
for b2 being Subset of b1
for b3 being non empty Subset of b1 holds b2 c= uparrow (b2 "/\" b3)
proof end;

theorem Th60: :: YELLOW_4:60
for b1 being non empty RelStr
for b2 being Subset of [:b1,b1:] holds union { b3 where B is Subset of b1 : ex b1 being Element of b1 st
( b3 = {b4} "/\" (proj2 b2) & b4 in proj1 b2 )
}
= (proj1 b2) "/\" (proj2 b2)
proof end;

theorem Th61: :: YELLOW_4:61
for b1 being transitive antisymmetric with_infima RelStr
for b2, b3 being Subset of b1 holds downarrow ((downarrow b2) "/\" (downarrow b3)) c= downarrow (b2 "/\" b3)
proof end;

theorem Th62: :: YELLOW_4:62
for b1 being Semilattice
for b2, b3 being Subset of b1 holds downarrow ((downarrow b2) "/\" (downarrow b3)) = downarrow (b2 "/\" b3)
proof end;

theorem Th63: :: YELLOW_4:63
for b1 being transitive antisymmetric with_infima RelStr
for b2, b3 being Subset of b1 holds uparrow ((uparrow b2) "/\" (uparrow b3)) c= uparrow (b2 "/\" b3)
proof end;

theorem Th64: :: YELLOW_4:64
for b1 being Semilattice
for b2, b3 being Subset of b1 holds uparrow ((uparrow b2) "/\" (uparrow b3)) = uparrow (b2 "/\" b3)
proof end;