ex p, q being Point of (Euclid n) st
( p = x & q = y & dist (x,y) = dist (p,q) ) by TOPREAL6:def 1;
hence 0 <= dist (x,y) ; :: according to XXREAL_0:def 7 :: thesis: verum