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