:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def 4 :
for L being non empty RelStr
for S being SubRelStr of L holds
( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );