let X be ComplexNormSpace; :: thesis: for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
let x, y be Point of X; :: thesis: ( ||.(x - y).|| > 0 iff x <> y )
( 0 < ||.(x - y).|| implies x - y <> 0. X ) by NORMSP_0:def 6;
hence ( 0 < ||.(x - y).|| implies x <> y ) by RLVECT_1:15; :: thesis: ( x <> y implies ||.(x - y).|| > 0 )

now :: thesis: ( x <> y implies 0 < ||.(x - y).|| )

assume x <> y ; :: thesis: 0 < ||.(x - y).||
then 0 <> ||.(x - y).|| by CLVECT_1:112;
hence 0 < ||.(x - y).|| by CLVECT_1:105; :: thesis: verum

end;

hence ( x <> y implies ||.(x - y).|| > 0 ) ; :: thesis: verum