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