theorem :: YELLOW_3:48

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