:: deftheorem DEFM defines Middle GTARSKI3:def 12 :
for S being TarskiGeometryStruct
for a, b, m being POINT of S holds
( Middle a,m,b iff ( between a,m,b & m,a equiv m,b ) );