theorem Th19: :: TOPREAL6:21

for A, B, C, D being set
for a, b being object st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))