let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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
; between m1,c,m2