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)) by Def7;
A3: p <> q by A1, Def7;
thus not p is_between q,r :: thesis: not r is_between p,q

proof

assume p is_between q,r ; :: thesis: contradiction
then dist (p,r) = (dist (p,q)) + ((dist (q,p)) + (dist (p,r))) by A2, Def7;
hence contradiction by A3, Th2; :: thesis: verum

end;

assume r is_between p,q ; :: thesis: contradiction
then A4: dist (p,q) = ((dist (p,q)) + (dist (q,r))) + (dist (r,q)) by A2, Def7;
q <> r by A1, Def7;
hence contradiction by A4, Th2; :: thesis: verum