theorem :: GTARSKI3:22
for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds
between5 e,d,c,b,a by Satz3p2;