theorem Th7: :: EUCLID12:8

for n being Nat
for Ln being Element of line_of_REAL n st Ln is being_line holds
for Pn being Element of REAL n holds not Ln = {Pn}