let S be satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st between a,b,c & between b,a,c holds
a = b
let a, b, c be POINT of S; :: thesis: ( between a,b,c & between b,a,c implies a = b )
assume ( between a,b,c & between b,a,c ) ; :: thesis: a = b
then consider x being POINT of S such that
A1: ( between b,x,b & between a,x,a ) by GTARSKI1:def 11;
( x = a & x = b ) by A1, GTARSKI1:def 10;
hence a = b ; :: thesis: verum