let p, q be Element of RealSpace; :: thesis: ( q >= p implies dist (p,q) = q - p )
assume p <= q ; :: thesis: dist (p,q) = q - p
then A1: q - p >= 0 by XREAL_1:48;
dist (p,q) = |.(q - p).| by TOPMETR:11
.= q - p by A1, ABSVALUE:def 1 ;
hence dist (p,q) = q - p ; :: thesis: verum