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 ) by Def7; :: according to SUB_METR:def 7 :: thesis: dist r,p = (dist r,q) + (dist q,p)
dist p,r = (dist p,q) + (dist q,r) by A1, Def7;
hence dist r,p = (dist r,q) + (dist q,p) ; :: thesis: verum