theorem :: YELLOW10:30

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