let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S
for A being Subset of S st between a,b,c & A is_line & a in A & c in A holds
b in A
let a, b, c be POINT of S; :: thesis: for A being Subset of S st between a,b,c & A is_line & a in A & c in A holds
b in A
let A be Subset of S; :: thesis: ( between a,b,c & A is_line & a in A & c in A implies b in A )
assume that
A1: between a,b,c and
A2: A is_line and
A3: a in A and
A4: c in A ; :: thesis: b in A
Collinear a,b,c by A1;
then Collinear a,c,b by GTARSKI3:45;
then A5: b in Line (a,c) ;
( a <> c or a = c ) ;
hence b in A by A2, A4, A5, GTARSKI3:87, A1, A3, GTARSKI1:def 10; :: thesis: verum