now

let x, y, z be Element of MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #); :: 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 x9 = x, y9 = y, z9 = z as Element of [:REAL ,REAL :] ;
A1: dist x,y = Eukl_dist2 . x9,y9 by METRIC_1:def 1;
hence ( dist x,y = 0 iff x = y ) by Th22; :: thesis: ( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )
dist y,x = Eukl_dist2 . y9,x9 by METRIC_1:def 1;
hence dist x,y = dist y,x by A1, Th23; :: thesis: dist x,z <= (dist x,y) + (dist y,z)
( dist x,z = Eukl_dist2 . x9,z9 & dist y,z = Eukl_dist2 . y9,z9 ) by METRIC_1:def 1;
hence dist x,z <= (dist x,y) + (dist y,z) by A1, Th24; :: thesis: verum

end;

hence MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #) is non empty strict MetrSpace by METRIC_1:6; :: thesis: verum