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 ;
take max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) ; :: thesis: S₁[x,y, max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 ))]
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] & max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) = 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] & max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) = 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] & max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) = 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 )] & max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) = 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 )] & max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) = max (the distance of M . (x `1 ),(y `1 )),(the distance of N . (x `2 ),(y `2 )) ) by MCART_1:23; :: 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