for n being Nat
for x1, x2 being Element of REAL n holds Line (x1,x2) in line_of_REAL n ;