theorem :: EUCLIDLP:60

for n being Nat
for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds
L0 // L2