theorem Th18: :: TOPREAL7:18

for M, N being non empty MetrStruct
for m1, m2 being Point of M
for n1, n2 being Point of N holds dist ([m1,n1],[m2,n2]) = max ((dist (m1,m2)),(dist (n1,n2)))