reconsider p = a, q = b as Point of (Euclid n) by TOPREAL3:13;
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