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