theorem Th37: :: YELLOW10:37

for S, T being non empty RelStr
for x being Element of [:S,T:] holds
( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )