theorem Satz6p17: :: GTARSKI3:83

for S being non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for p, q being POINT of S holds
( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )