theorem :: YELLOW10:35

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