theorem Th20: :: TOPREAL7:20

for M, N being non empty Reflexive MetrStruct holds max-Prod2 (M,N) is Reflexive