for p, q being Element of RealSpace st q >= p holds
dist (p,q) = q - p