let n be Nat; :: thesis: for L0, L1, L2 being Element of line_of_REAL n st L0 // L1 & L1 // L2 holds
L0 // L2
let L0, L1, L2 be Element of line_of_REAL n; :: thesis: ( L0 // L1 & L1 // L2 implies L0 // L2 )
assume that
A1: L0 // L1 and
A2: L1 // L2 ; :: thesis: L0 // L2
consider x0, x1, x2, x3 being Element of REAL n such that
A3: L0 = Line (x0,x1) and
A4: L1 = Line (x2,x3) and
A5: x1 - x0 // x3 - x2 by A1;
A6: x3 - x2 <> 0* n by A5;
consider y0, y1, y2, y3 being Element of REAL n such that
A7: L1 = Line (y0,y1) and
A8: L2 = Line (y2,y3) and
A9: y1 - y0 // y3 - y2 by A2;
A10: y1 - y0 <> 0* n by A9;
( x3 in Line (y1,y0) & x2 in Line (y1,y0) ) by A4, A7, EUCLID_4:9;
then ex a being Real st x3 - x2 = a * (y1 - y0) by Th31;
then x3 - x2 // y1 - y0 by A6, A10;
then x1 - x0 // y1 - y0 by A5, Th33;
then x1 - x0 // y3 - y2 by A9, Th33;
hence L0 // L2 by A3, A8; :: thesis: verum