theorem Th17: :: WAYBEL32:17

for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)