let M, N be non empty triangle MetrStruct ; :: thesis: max-Prod2 M,N is triangle
let a, b, c be Element of (max-Prod2 M,N); :: according to METRIC_1:def 6,METRIC_1:def 10 :: thesis: the distance of (max-Prod2 M,N) . a,c <= (the distance of (max-Prod2 M,N) . a,b) + (the distance of (max-Prod2 M,N) . b,c)
consider x1, y1 being Point of M, x2, y2 being Point of N such that
A1: a = [x1,x2] and
A2: b = [y1,y2] and
A3: 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
A4: b = [m1,m2] and
A5: c = [n1,n2] and
A6: the distance of (max-Prod2 M,N) . b,c = max (the distance of M . m1,n1),(the distance of N . m2,n2) by Def1;
A7: ( y1 = m1 & y2 = m2 ) by A2, A4, ZFMISC_1:33;
consider p1, q1 being Point of M, p2, q2 being Point of N such that
A8: a = [p1,p2] and
A9: c = [q1,q2] and
A10: the distance of (max-Prod2 M,N) . a,c = max (the distance of M . p1,q1),(the distance of N . p2,q2) by Def1;
A11: ( q1 = n1 & q2 = n2 ) by A5, A9, ZFMISC_1:33;
the distance of N is triangle by METRIC_1:def 10;
then A12: the distance of N . p2,q2 <= (the distance of N . p2,y2) + (the distance of N . y2,q2) by METRIC_1:def 6;
the distance of M is triangle by METRIC_1:def 10;
then A13: the distance of M . p1,q1 <= (the distance of M . p1,y1) + (the distance of M . y1,q1) by METRIC_1:def 6;
( x1 = p1 & x2 = p2 ) by A1, A8, ZFMISC_1:33;
hence the distance of (max-Prod2 M,N) . a,c <= (the distance of (max-Prod2 M,N) . a,b) + (the distance of (max-Prod2 M,N) . b,c) by A3, A6, A10, A13, A12, A7, A11, Th3; :: thesis: verum