let M, N be non empty symmetric MetrStruct ; :: thesis: max-Prod2 M,N is symmetric
let a, b be Element of (max-Prod2 M,N); :: according to METRIC_1:def 5,METRIC_1:def 9 :: thesis: the distance of (max-Prod2 M,N) . a,b = the distance of (max-Prod2 M,N) . b,a
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: ( a = [x1,x2] & b = [y1,y2] ) and
A2: the distance of (max-Prod2 M,N) . a,b = max (the distance of M . x1,y1),(the distance of N . x2,y2) by Def1;
consider m1, n1 being Point of M, m2, n2 being Point of N such that
A3: ( b = [m1,m2] & a = [n1,n2] ) and
A4: the distance of (max-Prod2 M,N) . b,a = max (the distance of M . m1,n1),(the distance of N . m2,n2) by Def1;
( the distance of M is symmetric & the distance of N is symmetric ) by METRIC_1:def 9;
then A5: ( the distance of M . x1,y1 = the distance of M . y1,x1 & the distance of N . x2,y2 = the distance of N . y2,x2 ) by METRIC_1:def 5;
( y1 = m1 & y2 = m2 & x1 = n1 & x2 = n2 ) by A1, A3, ZFMISC_1:33;
hence the distance of (max-Prod2 M,N) . a,b = the distance of (max-Prod2 M,N) . b,a by A2, A4, A5; :: thesis: verum