theorem Th32: :: YELLOW_3:32

for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 & y is_<=_than D2 )