theorem :: YELLOW10:26

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