theorem :: EUCLIDLP:78

for n being Nat
for x1, x2, x3, y2, y3 being Element of REAL n
for L1, L2 being Element of line_of_REAL n st x2 - x1,x3 - x1 are_lindependent2 & y2 in Line (x1,x2) & y3 in Line (x1,x3) & L1 = Line (x2,x3) & L2 = Line (y2,y3) holds
( L1 // L2 iff ex a being Real st
( a <> 0 & y2 - x1 = a * (x2 - x1) & y3 - x1 = a * (x3 - x1) ) )