let M, N be non empty MetrStruct ; :: thesis: 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)
let m1, m2 be Point of M; :: thesis: for n1, n2 being Point of N holds dist [m1,n1],[m2,n2] = max (dist m1,m2),(dist n1,n2)
let n1, n2 be Point of N; :: thesis: dist [m1,n1],[m2,n2] = max (dist m1,m2),(dist n1,n2)
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: ( [m1,n1] = [x1,x2] & [m2,n2] = [y1,y2] ) and
A2: the distance of (max-Prod2 M,N) . [m1,n1],[m2,n2] = max (the distance of M . x1,y1),(the distance of N . x2,y2) by Def1;
( m1 = x1 & n1 = x2 & m2 = y1 & n2 = y2 ) by A1, ZFMISC_1:33;
hence dist [m1,n1],[m2,n2] = max (dist m1,m2),(dist n1,n2) by A2; :: thesis: verum