theorem :: YELLOW10:42

for S being non empty RelStr
for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)