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 = abs (x - y) by Def13;
then x - y = 0 by ABSVALUE:2;
hence x = y ; :: thesis: verum

end;

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