theorem Th17: :: EUCLID12:22

for A being Point of (TOP-REAL 2)
for L1, L2 being Element of line_of_REAL 2 st L1 /\ L2 is being_point & A in L1 /\ L2 holds
L1 /\ L2 = {A} by TARSKI:def 1;