theorem :: GTARSKI3:66

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b <= c,d holds
b,a <= c,d by Satz2p4;