for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is directed iff downarrow X is directed )