defpred S₁[ 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₁[x,y,u]

proof

let x, y be Element of [: the carrier of M, the carrier of N:]; :: thesis: ex u being Element of REAL st S₁[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₁[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;

consider f being Function of [:[: the carrier of M, the carrier of N:],[: the carrier of M, the carrier of N:]:],REAL such that
A2: for x, y being Element of [: the carrier of M, the carrier of N:] holds S₁[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