theorem :: GTARSKI3:89

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, B being Subset of S
for a, b being POINT of S st A is_line & B is_line & A <> B & a in A & a in B & b in A & b in B holds
a = b by Satz6p19;