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 5,METRIC_1:def 9 :: 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, XTUPLE_0:1;

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, XTUPLE_0:1;

the distance of N is triangle by METRIC_1:def 9;

then A12: the distance of N . (p2,q2) <= ( the distance of N . (p2,y2)) + ( the distance of N . (y2,q2)) ;

the distance of M is triangle by METRIC_1:def 9;

then A13: the distance of M . (p1,q1) <= ( the distance of M . (p1,y1)) + ( the distance of M . (y1,q1)) ;

( x1 = p1 & x2 = p2 ) by A1, A8, XTUPLE_0:1;

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, Th2; :: thesis: verum

let a, b, c 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,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, XTUPLE_0:1;

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, XTUPLE_0:1;

the distance of N is triangle by METRIC_1:def 9;

then A12: the distance of N . (p2,q2) <= ( the distance of N . (p2,y2)) + ( the distance of N . (y2,q2)) ;

the distance of M is triangle by METRIC_1:def 9;

then A13: the distance of M . (p1,q1) <= ( the distance of M . (p1,y1)) + ( the distance of M . (y1,q1)) ;

( x1 = p1 & x2 = p2 ) by A1, A8, XTUPLE_0:1;

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, Th2; :: thesis: verum