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