let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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 holds
between b,A,c
let a, c, m, r be POINT of S; :: thesis: 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 holds
between b,A,c
let A be Subset of S; :: thesis: ( 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 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 ; :: thesis: for b being POINT of S st r out a,b holds
between b,A,c
let b be POINT of S; :: thesis: ( r out a,b implies between b,A,c )
assume A5: r out a,b ; :: thesis: between b,A,c

per cases then ( between r,b,a or between r,a,b ) ;

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

hence between b,A,c by A1, A2, A3, A4, A5, Th6; :: thesis: verum

end;

suppose A6: between r,a,b ; :: thesis: between b,A,c

set b9 = reflection (m,b);
set r9 = reflection (m,r);
A7: ( Middle b,m, reflection (m,b) & Middle r,m, reflection (m,r) ) by GTARSKI3:def 13;
A8: between reflection (m,r), reflection (m,a), reflection (m,b) by A6, GTARSKI3:106;
then A9: between reflection (m,r),c, reflection (m,b) by A3, GTARSKI3:def 13;
A10: ( A is_line & not b in A ) by A1, A4, A6, Th4;
G1: not reflection (m,b) in A

proof

assume A11: reflection (m,b) in A ; :: thesis: contradiction
reflection (m,b) <> m

proof

assume reflection (m,b) = m ; :: thesis: contradiction
then Middle b,m,m by GTARSKI3:100;
hence contradiction by A10, A2, GTARSKI1:def 7; :: thesis: verum

end;

hence contradiction by A10, A11, A7, A2, Th5, GTARSKI3:14; :: thesis: verum

end;

Middle reflection (m,b),m,b by GTARSKI3:def 13, GTARSKI3:96;
then U1: between reflection (m,b),A,b by A2, G1, A1, A4, A6, Th4;
U2: Middle reflection (m,b),m,b by GTARSKI3:96, GTARSKI3:def 13;
U3: reflection (m,r) in A by A4, GTARSKI3:104, A1, A2, A7, Th5;
then U4: reflection (m,r) out reflection (m,b),c by A9, A1, GTARSKI1:def 10;
between reflection (m,r),c, reflection (m,b) by A8, A3, GTARSKI3:def 13;
then between c,A,b by U1, U2, U3, U4, A2, Th6;
hence between b,A,c by GTARSKI3:14; :: thesis: verum

end;

end;