let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, c, r being POINT of S
for A being Subset of S st between2 a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between2 b,A,c
let a, c, r be POINT of S; :: thesis: for A being Subset of S st between2 a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between2 b,A,c
let A be Subset of S; :: thesis: ( between2 a,A,c & r in A implies for b being POINT of S st r out a,b holds
between2 b,A,c )
assume that
A1: between2 a,A,c and
A2: r in A ; :: thesis: for b being POINT of S st r out a,b holds
between2 b,A,c
consider t being POINT of S such that
A3: t in A and
A4: between a,t,c by A1;
A is_plane by A1;
then consider p9, q9, r9 being POINT of S such that
A5: not Collinear p9,q9,r9 and
A6: A = Plane (p9,q9,r9) ;

hereby :: thesis: verum

let b be POINT of S; :: thesis: ( r out a,b implies between2 b,A,c )
assume A7: r out a,b ; :: thesis: between2 b,A,c
A8: not b in A

proof

assume b in A ; :: thesis: contradiction
then T1: Line (r,b) c= A by A2, A7, A5, A6, Th69;
Collinear a,r,b by A7, GTARSKI3:73;
then Collinear r,b,a ;
then a in Line (r,b) ;
hence contradiction by T1, A1; :: thesis: verum

end;

thus between2 b,A,c :: thesis: verum

proof

per cases ( r = t or r <> t ) ;

suppose A10: r = t ; :: thesis: between2 b,A,c

between b,t,c

proof

per cases ( between r,b,a or between r,a,b ) by A7;

suppose between r,b,a ; :: thesis: between b,t,c

then ( between a,b,t & between a,t,c ) by A4, A10, GTARSKI3:14;
hence between b,t,c by GTARSKI3:18; :: thesis: verum

end;

suppose between r,a,b ; :: thesis: between b,t,c

then ( between b,a,t & between a,t,c & a <> t ) by A10, A4, A1, A3, GTARSKI3:14;
hence between b,t,c by GTARSKI3:19; :: thesis: verum

end;

end;

end;

hence between2 b,A,c by A1, A3, A8; :: thesis: verum

end;

suppose A11: r <> t ; :: thesis: between2 b,A,c

set L = Line (r,t);
A12: Line (r,t) c= A by A2, A11, A3, A5, A6, Th69;
( Line (r,t) is_line & not a in Line (r,t) & not c in Line (r,t) & ex t being POINT of S st
( t in Line (r,t) & between a,t,c ) ) by A1, A4, A11, A12, GTARSKI3:83;
then between a, Line (r,t),c ;
then between b, Line (r,t),c by A7, Th12, GTARSKI3:83;
hence between2 b,A,c by A1, A8, A12; :: thesis: verum

end;

end;

end;

end;