theorem :: YELLOW_3:49

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