for n being Nat
for L being Element of line_of_REAL n ex x being Element of REAL n st x in L