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:50;
dist p,q = abs (q - p) by TOPMETR:15
.= q - p by A1, ABSVALUE:def 1 ;
hence dist p,q = q - p ; :: thesis: verum