:: Metrics in the Cartesian Product - Part II
:: by Stanis\l awa Kanas and Adam Lecko
::
:: Received July 8, 1991
:: Copyright (c) 1991 Association of Mizar Users


definition
let X, Y be non empty MetrSpace;
func dist_cart2S X,Y -> Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:], REAL means :Def1: :: METRIC_4:def 1
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
it . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ));
existence
ex b1 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:], REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:], REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b2 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines dist_cart2S METRIC_4:def 1 :
for X, Y being non empty MetrSpace
for b3 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:], REAL holds
( b3 = dist_cart2S X,Y iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds
b3 . x,y = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) );

theorem :: METRIC_4:1
canceled;

theorem Th2: :: METRIC_4:2
for a, b being real number st 0 <= a & 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) )
proof end;

theorem Th3: :: METRIC_4:3
for X, Y being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y:] holds
( (dist_cart2S X,Y) . x,y = 0 iff x = y )
proof end;

theorem Th4: :: METRIC_4:4
for X, Y being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y:] holds (dist_cart2S X,Y) . x,y = (dist_cart2S X,Y) . y,x
proof end;

theorem Th5: :: METRIC_4:5
for a, b, c, d being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d holds
sqrt (((a + c) ^2 ) + ((b + d) ^2 )) <= (sqrt ((a ^2 ) + (b ^2 ))) + (sqrt ((c ^2 ) + (d ^2 )))
proof end;

theorem Th6: :: METRIC_4:6
for X, Y being non empty MetrSpace
for x, y, z being Element of [:the carrier of X,the carrier of Y:] holds (dist_cart2S X,Y) . x,z <= ((dist_cart2S X,Y) . x,y) + ((dist_cart2S X,Y) . y,z)
proof end;

definition
let X, Y be non empty MetrSpace;
let x, y be Element of [:the carrier of X,the carrier of Y:];
func dist2S x,y -> Real equals :: METRIC_4:def 2
(dist_cart2S X,Y) . x,y;
coherence
(dist_cart2S X,Y) . x,y is Real ;
end;

:: deftheorem defines dist2S METRIC_4:def 2 :
for X, Y being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y:] holds dist2S x,y = (dist_cart2S X,Y) . x,y;

definition
let X, Y be non empty MetrSpace;
func MetrSpaceCart2S X,Y -> non empty strict MetrSpace equals :: METRIC_4:def 3
 MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2S X,Y) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2S X,Y) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines MetrSpaceCart2S METRIC_4:def 3 :
for X, Y being non empty MetrSpace holds MetrSpaceCart2S X,Y = MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2S X,Y) #);

definition
let X, Y, Z be non empty MetrSpace;
func dist_cart3S X,Y,Z -> Function of [:[:the carrier of X,the carrier of Y,the carrier of Z:],[:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL means :Def4: :: METRIC_4:def 4
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
it . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 ));
existence
ex b1 being Function of [:[:the carrier of X,the carrier of Y,the carrier of Z:],[:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL st
for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of X,the carrier of Y,the carrier of Z:],[:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL st ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) ) & ( for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b2 . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist_cart3S METRIC_4:def 4 :
for X, Y, Z being non empty MetrSpace
for b4 being Function of [:[:the carrier of X,the carrier of Y,the carrier of Z:],[:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL holds
( b4 = dist_cart3S X,Y,Z iff for x1, y1 being Element of X
for x2, y2 being Element of Y
for x3, y3 being Element of Z
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b4 . x,y = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) );

theorem :: METRIC_4:7
canceled;

theorem :: METRIC_4:8
canceled;

theorem :: METRIC_4:9
canceled;

theorem Th10: :: METRIC_4:10
for X, Y, Z being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds
( (dist_cart3S X,Y,Z) . x,y = 0 iff x = y )
proof end;

theorem Th11: :: METRIC_4:11
for X, Y, Z being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds (dist_cart3S X,Y,Z) . x,y = (dist_cart3S X,Y,Z) . y,x
proof end;

theorem :: METRIC_4:12
for a, b, c being complex number holds ((a + b) + c) ^2 = (((a ^2 ) + (b ^2 )) + (c ^2 )) + ((((2 * a) * b) + ((2 * a) * c)) + ((2 * b) * c)) ;

theorem Th13: :: METRIC_4:13
for a, b, c, d, e, f being real number holds (((2 * (a * d)) * (c * b)) + ((2 * (a * f)) * (e * c))) + ((2 * (b * f)) * (e * d)) <= ((((((a * d) ^2 ) + ((c * b) ^2 )) + ((a * f) ^2 )) + ((e * c) ^2 )) + ((b * f) ^2 )) + ((e * d) ^2 )
proof end;

theorem :: METRIC_4:14
canceled;

theorem Th15: :: METRIC_4:15
for a, b, c, d, e, f being real number holds (((a * c) + (b * d)) + (e * f)) ^2 <= (((a ^2 ) + (b ^2 )) + (e ^2 )) * (((c ^2 ) + (d ^2 )) + (f ^2 ))
proof end;

Lm1: for a, b, c, d, e, f being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f holds
sqrt ((((a + c) ^2 ) + ((b + d) ^2 )) + ((e + f) ^2 )) <= (sqrt (((a ^2 ) + (b ^2 )) + (e ^2 ))) + (sqrt (((c ^2 ) + (d ^2 )) + (f ^2 )))
proof end;

theorem Th16: :: METRIC_4:16
for X, Y, Z being non empty MetrSpace
for x, y, z being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds (dist_cart3S X,Y,Z) . x,z <= ((dist_cart3S X,Y,Z) . x,y) + ((dist_cart3S X,Y,Z) . y,z)
proof end;

definition
let X, Y, Z be non empty MetrSpace;
let x, y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:];
func dist3S x,y -> Real equals :: METRIC_4:def 5
(dist_cart3S X,Y,Z) . x,y;
coherence
(dist_cart3S X,Y,Z) . x,y is Real ;
end;

:: deftheorem defines dist3S METRIC_4:def 5 :
for X, Y, Z being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist3S x,y = (dist_cart3S X,Y,Z) . x,y;

definition
let X, Y, Z be non empty MetrSpace;
func MetrSpaceCart3S X,Y,Z -> non empty strict MetrSpace equals :: METRIC_4:def 6
 MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines MetrSpaceCart3S METRIC_4:def 6 :
for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3S X,Y,Z = MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #);

theorem :: METRIC_4:17
canceled;

theorem :: METRIC_4:18
canceled;

definition
func taxi_dist2 -> Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL means :Def7: :: METRIC_4:def 7
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
it . x,y = (real_dist . x1,y1) + (real_dist . x2,y2);
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2)
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b2 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines taxi_dist2 METRIC_4:def 7 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL holds
( b1 = taxi_dist2 iff for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) );

theorem Th19: :: METRIC_4:19
for x, y being Element of [:REAL ,REAL :] holds
( taxi_dist2 . x,y = 0 iff x = y )
proof end;

theorem Th20: :: METRIC_4:20
for x, y being Element of [:REAL ,REAL :] holds taxi_dist2 . x,y = taxi_dist2 . y,x
proof end;

theorem Th21: :: METRIC_4:21
for x, y, z being Element of [:REAL ,REAL :] holds taxi_dist2 . x,z <= (taxi_dist2 . x,y) + (taxi_dist2 . y,z)
proof end;

definition
func RealSpaceCart2 -> non empty strict MetrSpace equals :: METRIC_4:def 8
 MetrStruct(# [:REAL ,REAL :],taxi_dist2 #);
coherence
MetrStruct(# [:REAL ,REAL :],taxi_dist2 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines RealSpaceCart2 METRIC_4:def 8 :
RealSpaceCart2 = MetrStruct(# [:REAL ,REAL :],taxi_dist2 #);

definition
func Eukl_dist2 -> Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL means :Def9: :: METRIC_4:def 9
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
it . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 ));
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st
for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL st ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) ) & ( for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b2 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Eukl_dist2 METRIC_4:def 9 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:], REAL holds
( b1 = Eukl_dist2 iff for x1, y1, x2, y2 being Element of REAL
for x, y being Element of [:REAL ,REAL :] st x = [x1,x2] & y = [y1,y2] holds
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) );

theorem Th22: :: METRIC_4:22
for x, y being Element of [:REAL ,REAL :] holds
( Eukl_dist2 . x,y = 0 iff x = y )
proof end;

theorem Th23: :: METRIC_4:23
for x, y being Element of [:REAL ,REAL :] holds Eukl_dist2 . x,y = Eukl_dist2 . y,x
proof end;

theorem Th24: :: METRIC_4:24
for x, y, z being Element of [:REAL ,REAL :] holds Eukl_dist2 . x,z <= (Eukl_dist2 . x,y) + (Eukl_dist2 . y,z)
proof end;

definition
func EuklSpace2 -> non empty strict MetrSpace equals :: METRIC_4:def 10
 MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #);
coherence
MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines EuklSpace2 METRIC_4:def 10 :
EuklSpace2 = MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #);

definition
func taxi_dist3 -> Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL means :Def11: :: METRIC_4:def 11
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
it . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3);
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3)
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) ) & ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b2 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines taxi_dist3 METRIC_4:def 11 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL holds
( b1 = taxi_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) );

theorem Th25: :: METRIC_4:25
for x, y being Element of [:REAL ,REAL ,REAL :] holds
( taxi_dist3 . x,y = 0 iff x = y )
proof end;

theorem Th26: :: METRIC_4:26
for x, y being Element of [:REAL ,REAL ,REAL :] holds taxi_dist3 . x,y = taxi_dist3 . y,x
proof end;

theorem Th27: :: METRIC_4:27
for x, y, z being Element of [:REAL ,REAL ,REAL :] holds taxi_dist3 . x,z <= (taxi_dist3 . x,y) + (taxi_dist3 . y,z)
proof end;

definition
func RealSpaceCart3 -> non empty strict MetrSpace equals :: METRIC_4:def 12
 MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #);
coherence
MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines RealSpaceCart3 METRIC_4:def 12 :
RealSpaceCart3 = MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #);

definition
func Eukl_dist3 -> Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL means :Def13: :: METRIC_4:def 13
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
it . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ));
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st
for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ))
proof end;
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL st ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) & ( for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b2 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Eukl_dist3 METRIC_4:def 13 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:], REAL holds
( b1 = Eukl_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL ,REAL ,REAL :] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) );

theorem Th28: :: METRIC_4:28
for x, y being Element of [:REAL ,REAL ,REAL :] holds
( Eukl_dist3 . x,y = 0 iff x = y )
proof end;

theorem Th29: :: METRIC_4:29
for x, y being Element of [:REAL ,REAL ,REAL :] holds Eukl_dist3 . x,y = Eukl_dist3 . y,x
proof end;

theorem Th30: :: METRIC_4:30
for x, y, z being Element of [:REAL ,REAL ,REAL :] holds Eukl_dist3 . x,z <= (Eukl_dist3 . x,y) + (Eukl_dist3 . y,z)
proof end;

definition
func EuklSpace3 -> non empty strict MetrSpace equals :: METRIC_4:def 14
 MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #);
coherence
MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines EuklSpace3 METRIC_4:def 14 :
EuklSpace3 = MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #);