let S be MetrSpace; :: thesis: for p, q, r being Element of S st q is_between p,r holds

( not p is_between q,r & not r is_between p,q )

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

assume A1: q is_between p,r ; :: thesis: ( not p is_between q,r & not r is_between p,q )

then A2: dist (p,r) = (dist (p,q)) + (dist (q,r)) ;

thus not p is_between q,r by A2, Th7; :: thesis: not r is_between p,q

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

then A3: dist (p,q) = ((dist (p,q)) + (dist (q,r))) + (dist (r,q)) by A2;

q <> r by A1;

hence contradiction by A3, Th7; :: thesis: verum

( not p is_between q,r & not r is_between p,q )

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

assume A1: q is_between p,r ; :: thesis: ( not p is_between q,r & not r is_between p,q )

then A2: dist (p,r) = (dist (p,q)) + (dist (q,r)) ;

thus not p is_between q,r by A2, Th7; :: thesis: not r is_between p,q

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

then A3: dist (p,q) = ((dist (p,q)) + (dist (q,r))) + (dist (r,q)) by A2;

q <> r by A1;

hence contradiction by A3, Th7; :: thesis: verum