theorem :: WAYBEL_0:7

for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )