theorem Th6: :: EUCLID12:6

for n being Nat
for Ln being Element of line_of_REAL n holds
( Ln is being_line or ex Pn being Element of REAL n st Ln = {Pn} )