theorem :: YELLOW10:31

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