for R, S being non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr st the carrier of R /\ the carrier of S is non empty directed lower Subset of S holds
Bottom S in the carrier of R