let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds
( x <> y iff dist x,y > 0 )
let x, y be Point of X; :: thesis: ( x <> y iff dist x,y > 0 )
thus ( x <> y implies dist x,y > 0 ) :: thesis: ( dist x,y > 0 implies x <> y )

proof

assume x <> y ; :: thesis: dist x,y > 0
then dist x,y <> 0 by Th43;
hence dist x,y > 0 by Th34; :: thesis: verum

end;

thus ( dist x,y > 0 implies x <> y ) by Th41; :: thesis: verum