let S be MetrSpace; :: thesis: for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds
( q is_between p,s & r is_between q,s )
let p, q, r, s be Element of S; :: thesis: ( q is_between p,r & r is_between p,s implies ( q is_between p,s & r is_between q,s ) )
assume A1: q is_between p,r ; :: thesis: ( not r is_between p,s or ( q is_between p,s & r is_between q,s ) )
then A2: p <> q ;
assume A3: r is_between p,s ; :: thesis: ( q is_between p,s & r is_between q,s )
then A4: ( p <> s & r <> s ) ;
dist (p,r) = (dist (p,q)) + (dist (q,r)) by A1;
then A5: dist (p,s) = ((dist (p,q)) + (dist (q,r))) + (dist (r,s)) by A3;
( dist (p,s) <= (dist (p,q)) + (dist (q,s)) & (dist (p,q)) + (dist (q,s)) <= ((dist (q,r)) + (dist (r,s))) + (dist (p,q)) ) by Th4, XREAL_1:6;
then A6: (dist (p,q)) + (dist (q,s)) = (dist (p,q)) + ((dist (q,r)) + (dist (r,s))) by A5, XXREAL_0:1;
A7: q <> r by A1;
then q <> s by A5, Th7;
hence ( q is_between p,s & r is_between q,s ) by A2, A7, A4, A5, A6; :: thesis: verum