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