theorem :: YELLOW10:34

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