let n be Element of 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 A1: ( L0 // L1 & L1 // L2 ) ; :: thesis: L0 // L2
then consider x0, x1, x2, x3 being Element of REAL n such that
A2: ( L0 = Line x0,x1 & L1 = Line x2,x3 & x1 - x0 // x3 - x2 ) by Def7;
consider y0, y1, y2, y3 being Element of REAL n such that
A3: ( L1 = Line y0,y1 & L2 = Line y2,y3 & y1 - y0 // y3 - y2 ) by A1, Def7;
A4: ( x3 - x2 <> 0* n & y1 - y0 <> 0* n ) by A2, A3, Def1;
( x3 in Line y1,y0 & x2 in Line y1,y0 ) by A2, A3, EUCLID_4:10;
then consider a being Real such that
A5: x3 - x2 = a * (y1 - y0) by Th36;
x3 - x2 // y1 - y0 by A4, A5, Def1;
then x1 - x0 // y1 - y0 by A2, Th38;
then ( L0 = Line x0,x1 & L2 = Line y2,y3 & x1 - x0 // y3 - y2 ) by A2, A3, Th38;
hence L0 // L2 by Def7; :: thesis: verum