reconsider p = a, q = b as Point of (Euclid n) by TOPREAL3:8;
take dist (p,q) ; :: thesis: ex p, q being Point of (Euclid n) st
( p = a & q = b & dist (p,q) = dist (p,q) )
thus ex p, q being Point of (Euclid n) st
( p = a & q = b & dist (p,q) = dist (p,q) ) ; :: thesis: verum