theorem Th28: :: YELLOW10:28

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