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