theorem :: GTARSKI3:96

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, m being POINT of S st Middle a,m,b holds
Middle b,m,a by Satz3p2, Satz2p2;