:: deftheorem defines Midpoint GTARSKI4:def 9 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, b₄ being POINT of S holds
( b₄ = Midpoint (a,b) iff Middle a,b₄,b );