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