let x, y be Element of [:REAL ,REAL ,REAL :]; :: thesis: ( Eukl_dist3 . x,y = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , x3 = x `3 , y1 = y `1 , y2 = y `2 , y3 = y `3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:48;
thus ( Eukl_dist3 . x,y = 0 implies x = y ) :: thesis: ( x = y implies Eukl_dist3 . x,y = 0 )

proof

set d3 = real_dist . x3,y3;
set d2 = real_dist . x2,y2;
set d1 = real_dist . x1,y1;
A2: ( 0 <= (real_dist . x2,y2) ^2 & 0 <= (real_dist . x3,y3) ^2 ) by XREAL_1:65;
assume Eukl_dist3 . x,y = 0 ; :: thesis: x = y
then sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) = 0 by A1, Def13;
then A3: sqrt (((real_dist . x1,y1) ^2 ) + (((real_dist . x2,y2) ^2 ) + ((real_dist . x3,y3) ^2 ))) = 0 ;
( 0 <= (real_dist . x2,y2) ^2 & 0 <= (real_dist . x3,y3) ^2 ) by XREAL_1:65;
then A4: ( 0 <= (real_dist . x1,y1) ^2 & 0 + 0 <= ((real_dist . x2,y2) ^2 ) + ((real_dist . x3,y3) ^2 ) ) by XREAL_1:9, XREAL_1:65;
then real_dist . x1,y1 = 0 by A3, Th2;
then A5: x1 = y1 by METRIC_1:9;
A6: ((real_dist . x2,y2) ^2 ) + ((real_dist . x3,y3) ^2 ) = 0 by A3, A4, Th2;
then real_dist . x2,y2 = 0 by A2, XREAL_1:29;
then A7: x2 = y2 by METRIC_1:9;
real_dist . x3,y3 = 0 by A6, A2, XREAL_1:29;
hence x = y by A1, A5, A7, METRIC_1:9; :: thesis: verum

end;

assume A8: x = y ; :: thesis: Eukl_dist3 . x,y = 0
then A9: ( (real_dist . x1,y1) ^2 = 0 ^2 & (real_dist . x2,y2) ^2 = 0 ^2 ) by METRIC_1:9;
Eukl_dist3 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) by A1, Def13
.= 0 ^2 by A8, A9, METRIC_1:9, SQUARE_1:82 ;
hence Eukl_dist3 . x,y = 0 ; :: thesis: verum