theorem :: YELLOW10:27

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