let a, b, c be POINT of TarskiEuclid2Space; :: thesis: ( between a,b,c iff dist (a,c) = (dist (a,b)) + (dist (b,c)) )

hereby :: thesis: ( dist (a,c) = (dist (a,b)) + (dist (b,c)) implies between a,b,c )

assume between a,b,c ; :: thesis: dist (a,c) = (dist (a,b)) + (dist (b,c))
then b is_Between a,c by GTARSKI1:def 15;
hence dist (a,c) = (dist (a,b)) + (dist (b,c)) ; :: thesis: verum

end;

assume dist (a,c) = (dist (a,b)) + (dist (b,c)) ; :: thesis: between a,b,c
then b is_Between a,c ;
hence between a,b,c by GTARSKI1:def 15; :: thesis: verum