let x, y be Element of REAL ; :: thesis: ( real_dist . (x,y) = 0 iff x = y )
thus ( real_dist . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies real_dist . (x,y) = 0 )

proof

assume real_dist . (x,y) = 0 ; :: thesis: x = y
then 0 = |.(x - y).| by Def12;
then x - y = 0 by ABSVALUE:2;
hence x = y ; :: thesis: verum

end;

assume x = y ; :: thesis: real_dist . (x,y) = 0
then |.(x - y).| = 0 by ABSVALUE:2;
hence real_dist . (x,y) = 0 by Def12; :: thesis: verum