theorem Satz7p3: :: GTARSKI3:97

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct
for a, m being POINT of S holds
( Middle a,m,a iff m = a ) by GTARSKI1:def 10, Satz3p1, Satz2p1;