let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for a, c, m, r being POINT of S
for A being Subset of S st between a,A,c & m in A & Middle a,m,c & r in A holds
for b being POINT of S st r out a,b & between r,b,a holds
between b,A,c
let a, c, m, r be POINT of S; for A being Subset of S st between a,A,c & m in A & Middle a,m,c & r in A holds
for b being POINT of S st r out a,b & between r,b,a holds
between b,A,c
let A be Subset of S; ( between a,A,c & m in A & Middle a,m,c & r in A implies for b being POINT of S st r out a,b & between r,b,a holds
between b,A,c )
assume that
A1:
between a,A,c
and
A2:
m in A
and
A3:
Middle a,m,c
and
A4:
r in A
; for b being POINT of S st r out a,b & between r,b,a holds
between b,A,c
A5:
between c,m,a
by A3, GTARSKI3:14;
let b be POINT of S; ( r out a,b & between r,b,a implies between b,A,c )
assume that
A6:
r out a,b
and
A7:
between r,b,a
; between b,A,c
consider t being POINT of S such that
A8:
between b,t,c
and
A9:
between m,t,r
by A7, A5, GTARSKI1:def 11;
Collinear r,b,a
by A7;
then
a in Line (r,b)
;
hence
between b,A,c
by A8, A9, A2, Th4, A1, A4, A6, GTARSKI3:87; verum