let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 holds
between m1,c,m2
let c, a1, a2, b1, b2, m1, m2 be POINT of S; :: thesis: ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 implies between m1,c,m2 )
assume that
A1: between a1,c,a2 and
A2: between b1,c,b2 and
A3: c,a1 equiv c,b1 and
A4: c,a2 equiv c,b2 and
A5: Middle a1,m1,b1 and
A6: Middle a2,m2,b2 ; :: thesis: between m1,c,m2

per cases ( c,a1 <= c,a2 or c,a2 <= c,a1 ) by Satz5p10;

suppose c,a1 <= c,a2 ; :: thesis: between m1,c,m2

hence between m1,c,m2 by A1, A2, A3, A4, A5, A6, Satz7p22part1; :: thesis: verum

end;

suppose c,a2 <= c,a1 ; :: thesis: between m1,c,m2

hence between m1,c,m2 by A1, A2, A3, A4, A5, A6, Satz7p22part2; :: thesis: verum

end;

end;