theorem Th30: :: WAYBEL_0:30

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