theorem :: EUCLID12:7

for n being Nat
for Ln being Element of line_of_REAL n holds
( Ln is being_line or Ln is being_point ) by Th6;