defpred S_{1}[ set , set , set ] means ex x1, y1 being Point of M ex x2, y2 being Point of N st

( $1 = [x1,x2] & $2 = [y1,y2] & $3 = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) );

set C = [: the carrier of M, the carrier of N:];

A1: for x, y being Element of [: the carrier of M, the carrier of N:] ex u being Element of REAL st S_{1}[x,y,u]

A2: for x, y being Element of [: the carrier of M, the carrier of N:] holds S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);

take E = MetrStruct(# [: the carrier of M, the carrier of N:],f #); :: thesis: ( the carrier of E = [: the carrier of M, the carrier of N:] & ( for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )

thus the carrier of E = [: the carrier of M, the carrier of N:] ; :: thesis: for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

let x, y be Point of E; :: thesis: ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A3: ( x = [x1,x2] & y = [y1,y2] & f . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A2;

take x1 ; :: thesis: ex y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take y1 ; :: thesis: ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take x2 ; :: thesis: ex y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take y2 ; :: thesis: ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

thus ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A3; :: thesis: verum

( $1 = [x1,x2] & $2 = [y1,y2] & $3 = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) );

set C = [: the carrier of M, the carrier of N:];

A1: for x, y being Element of [: the carrier of M, the carrier of N:] ex u being Element of REAL st S

proof

consider f being Function of [:[: the carrier of M, the carrier of N:],[: the carrier of M, the carrier of N:]:],REAL such that
let x, y be Element of [: the carrier of M, the carrier of N:]; :: thesis: ex u being Element of REAL st S_{1}[x,y,u]

set x1 = x `1 ;

set x2 = x `2 ;

set y1 = y `1 ;

set y2 = y `2 ;

set m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2))));

reconsider m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) as Element of REAL by XREAL_0:def 1;

take m ; :: thesis: S_{1}[x,y,m]

take x `1 ; :: thesis: ex y1 being Point of M ex x2, y2 being Point of N st

( x = [(x `1),x2] & y = [y1,y2] & m = max (( the distance of M . ((x `1),y1)),( the distance of N . (x2,y2))) )

take y `1 ; :: thesis: ex x2, y2 being Point of N st

( x = [(x `1),x2] & y = [(y `1),y2] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . (x2,y2))) )

take x `2 ; :: thesis: ex y2 being Point of N st

( x = [(x `1),(x `2)] & y = [(y `1),y2] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),y2))) )

take y `2 ; :: thesis: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) )

thus ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ) by MCART_1:21; :: thesis: verum

end;set x1 = x `1 ;

set x2 = x `2 ;

set y1 = y `1 ;

set y2 = y `2 ;

set m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2))));

reconsider m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) as Element of REAL by XREAL_0:def 1;

take m ; :: thesis: S

take x `1 ; :: thesis: ex y1 being Point of M ex x2, y2 being Point of N st

( x = [(x `1),x2] & y = [y1,y2] & m = max (( the distance of M . ((x `1),y1)),( the distance of N . (x2,y2))) )

take y `1 ; :: thesis: ex x2, y2 being Point of N st

( x = [(x `1),x2] & y = [(y `1),y2] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . (x2,y2))) )

take x `2 ; :: thesis: ex y2 being Point of N st

( x = [(x `1),(x `2)] & y = [(y `1),y2] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),y2))) )

take y `2 ; :: thesis: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) )

thus ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] & m = max (( the distance of M . ((x `1),(y `1))),( the distance of N . ((x `2),(y `2)))) ) by MCART_1:21; :: thesis: verum

A2: for x, y being Element of [: the carrier of M, the carrier of N:] holds S

take E = MetrStruct(# [: the carrier of M, the carrier of N:],f #); :: thesis: ( the carrier of E = [: the carrier of M, the carrier of N:] & ( for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) ) )

thus the carrier of E = [: the carrier of M, the carrier of N:] ; :: thesis: for x, y being Point of E ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

let x, y be Point of E; :: thesis: ex x1, y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

consider x1, y1 being Point of M, x2, y2 being Point of N such that

A3: ( x = [x1,x2] & y = [y1,y2] & f . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A2;

take x1 ; :: thesis: ex y1 being Point of M ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take y1 ; :: thesis: ex x2, y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take x2 ; :: thesis: ex y2 being Point of N st

( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

take y2 ; :: thesis: ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) )

thus ( x = [x1,x2] & y = [y1,y2] & the distance of E . (x,y) = max (( the distance of M . (x1,y1)),( the distance of N . (x2,y2))) ) by A3; :: thesis: verum