let p, q be Point of (TOP-REAL 2); :: thesis: ( p <> q implies dist (p,q) > 0 )
ex p9, q9 being Point of (Euclid 2) st
( p9 = p & q9 = q & dist (p,q) = dist (p9,q9) ) by TOPREAL6:def 1;
hence ( p <> q implies dist (p,q) > 0 ) by METRIC_1:7; :: thesis: verum