:: deftheorem defines Line EUCLID_4:def 1 :
for n being Nat
for x1, x2 being Element of REAL n holds Line (x1,x2) = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ;