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 )

then |.(x - y).| = 0 by ABSVALUE:2;

hence real_dist . (x,y) = 0 by Def12; :: thesis: verum

thus ( real_dist . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies real_dist . (x,y) = 0 )

proof

assume
x = y
; :: thesis: real_dist . (x,y) = 0
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;then 0 = |.(x - y).| by Def12;

then x - y = 0 by ABSVALUE:2;

hence x = y ; :: thesis: verum

then |.(x - y).| = 0 by ABSVALUE:2;

hence real_dist . (x,y) = 0 by Def12; :: thesis: verum