:: deftheorem defines line_of_REAL EUCLIDLP:def 4 :
for n being Nat holds line_of_REAL n = { (Line (x1,x2)) where x1, x2 is Element of REAL n : verum } ;