theorem :: GTARSKI3:46

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct
for a, b being POINT of S holds Collinear a,a,b by Satz3p1;