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 by Def7;
assume A3: r is_between p,s ; :: thesis: ( q is_between p,s & r is_between q,s )
then A4: ( p <> s & r <> s ) by Def7;
dist p,r = (dist p,q) + (dist q,r) by A1, Def7;
then A5: dist p,s = ((dist p,q) + (dist q,r)) + (dist r,s) by A3, Def7;
dist q,s <= (dist q,r) + (dist r,s) by METRIC_1:4;
then ( 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 METRIC_1:4, XREAL_1:8;
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, Def7;
then q <> s by A5, METRIC_1:2;
hence ( q is_between p,s & r is_between q,s ) by A2, A7, A4, A5, A6, Def7; :: thesis: verum