theorem :: YELLOW10:32

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