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