now let x,
y,
z be
Element of
MetrStruct(#
[:REAL ,REAL ,REAL :],
taxi_dist3 #);
:: thesis: ( ( dist x,y = 0 implies x = y ) & ( x = y implies dist x,y = 0 ) & dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )reconsider x' =
x,
y' =
y,
z' =
z as
Element of
[:REAL ,REAL ,REAL :] ;
A1:
dist x,
y = taxi_dist3 . x',
y'
by METRIC_1:def 1;
A2:
dist x,
z = taxi_dist3 . x',
z'
by METRIC_1:def 1;
A3:
dist y,
z = taxi_dist3 . y',
z'
by METRIC_1:def 1;
A4:
dist y,
x = taxi_dist3 . y',
x'
by METRIC_1:def 1;
thus
(
dist x,
y = 0 iff
x = y )
by A1, Th25;
:: thesis: ( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )thus
dist x,
y = dist y,
x
by A1, A4, Th26;
:: thesis: dist x,z <= (dist x,y) + (dist y,z)thus
dist x,
z <= (dist x,y) + (dist y,z)
by A1, A2, A3, Th27;
:: thesis: verum end;
hence
MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #) is non empty strict MetrSpace
by METRIC_1:6; :: thesis: verum