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