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