theorem :: YELLOW_3:22

for S1, S2 being non empty reflexive RelStr
for D being non empty directed Subset of [:S1,S2:] holds
( proj1 D is directed & proj2 D is directed )