for S being RelStr
for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)