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