for n being Nat
for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st L is being_line & L = Line (x1,x2) holds
x1 <> x2