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