let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, p being POINT of S st between a,p,c & p out a,b holds
between b,p,c
let a, b, c, p be POINT of S; :: thesis: ( between a,p,c & p out a,b implies between b,p,c )
assume that
A1: between a,p,c and
A2: p out a,b ; :: thesis: between b,p,c
( p = c or p <> c ) ;
hence between b,p,c by A1, A2, GTARSKI3:13, GTARSKI3:71; :: thesis: verum