let S be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for p, q, r being Element of S st q is_between p,r holds

q is_between r,p

let p, q, r be Element of S; :: thesis: ( q is_between p,r implies q is_between r,p )

assume A1: q is_between p,r ; :: thesis: q is_between r,p

hence ( r <> q & r <> p & q <> p ) ; :: according to METRIC_1:def 22 :: thesis: dist (r,p) = (dist (r,q)) + (dist (q,p))

dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1;

hence dist (r,p) = (dist (r,q)) + (dist (q,p)) ; :: thesis: verum

q is_between r,p

let p, q, r be Element of S; :: thesis: ( q is_between p,r implies q is_between r,p )

assume A1: q is_between p,r ; :: thesis: q is_between r,p

hence ( r <> q & r <> p & q <> p ) ; :: according to METRIC_1:def 22 :: thesis: dist (r,p) = (dist (r,q)) + (dist (q,p))

dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1;

hence dist (r,p) = (dist (r,q)) + (dist (q,p)) ; :: thesis: verum