:: deftheorem Def10 defines "/\" YELLOW_0:def 10 :
for L being RelStr
for X being set
for b₃ being Element of L st ex_inf_of X,L holds
( b₃ = "/\" (X,L) iff ( X is_>=_than b₃ & ( for a being Element of L st X is_>=_than a holds
a <= b₃ ) ) );