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

( 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