for n being Nat
for L being Element of line_of_REAL n ex x1, x2 being Element of REAL n st L = Line (x1,x2)