let S be MetrSpace; 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; ( 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
; ( 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; not r is_between p,q
assume
r is_between p,q
; 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; verum