let n be Element of NAT ; :: thesis: for L, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds
L1 // L2
let L, L1, L2 be Element of line_of_REAL n; :: thesis: for P being Element of plane_of_REAL n st L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 holds
L1 // L2
let P be Element of plane_of_REAL n; :: thesis: ( L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2 )
assume A1: ( L c= P & L1 c= P & L2 c= P ) ; :: thesis: ( not L _|_ L1 or not L _|_ L2 or L1 // L2 )
then A2: ( L,L1 are_coplane & L,L2 are_coplane & L1,L2 are_coplane ) by Th101;
assume A3: ( L _|_ L1 & L _|_ L2 ) ; :: thesis: L1 // L2
then A4: ( L meets L1 & L meets L2 ) by A2, Th114;
then consider x1 being Element of REAL n such that
A5: ( x1 in L & x1 in L1 ) by Th54;
consider x2 being Element of REAL n such that
A6: ( x2 in L & x2 in L2 ) by A4, Th54;
A7: ( L is being_line & L1 is being_line & L2 is being_line ) by A3, Th72;

now

per cases ( x1 = x2 or x1 <> x2 ) ;

case x1 = x2 ; :: thesis: L1 // L2

hence L1 // L2 by A1, A3, A5, A6, A7, Th70, Th113; :: thesis: verum

end;

case A8: x1 <> x2 ; :: thesis: L1 // L2

consider x0 being Element of REAL n such that
A9: ( x0 <> x1 & x0 in L1 ) by A5, A7, Th58;
consider x being Element of REAL n such that
A10: ( x <> x2 & x in L2 ) by A6, A7, Th58;
A11: x0 - x1 _|_ x2 - x1 by A3, A5, A6, A8, A9, Th79;
then P = plane x1,x0,x2 by A1, A5, A6, A9, Th50, Th97;
then consider a1, a3, a2 being Real such that
A12: ( (a1 + a3) + a2 = 1 & x = ((a1 * x1) + (a3 * x0)) + (a2 * x2) ) by A1, A10, Th93;
A13: (a2 + a1) + a3 = 1 by A12;
A14: x - x2 = (- x2) + (((a2 * x2) + (a1 * x1)) + (a3 * x0)) by A12, RVSUM_1:32
.= (- x2) + ((x2 + (a1 * (x1 - x2))) + (a3 * (x0 - x2))) by A13, Th32
.= (- x2) + (x2 + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))) by RVSUM_1:32
.= ((- x2) + x2) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by RVSUM_1:32
.= (0* n) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by Th7
.= (a1 * (x1 - x2)) + (a3 * (x0 - x2)) by EUCLID_4:1 ;
x - x2 _|_ x1 - x2 by A3, A5, A6, A8, A10, Th79;
then A15: x - x2,x1 - x2 are_orthogonal by Def3;
x0 - x1,x2 - x1 are_orthogonal by A11, Def3;
then A16: |((x0 - x1),(x2 - x1))| = 0 by EUCLID_2:def 3;
A17: |((x0 - x1),(x1 - x2))| = |((x0 - x1),(((- 1) * x2) + (- (- x1))))|
.= |((x0 - x1),((- 1) * (x2 + (- x1))))| by EUCLID_4:6
.= (- 1) * |((x0 - x1),(x2 - x1))| by EUCLID_4:27
.= 0 by A16 ;
A18: x0 - x2 = x0 - ((0* n) + x2) by EUCLID_4:1
.= x0 - ((x1 - x1) + x2) by Th7
.= (x0 - (x1 - x1)) - x2 by RVSUM_1:60
.= ((x0 - x1) + x1) - x2 by Th9
.= (x0 - x1) + (x1 - x2) by Th10 ;
A19: 0 = |(((a1 * (x1 - x2)) + (a3 * (x0 - x2))),(x1 - x2))| by A14, A15, EUCLID_2:def 3
.= |((a1 * (x1 - x2)),(x1 - x2))| + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:25
.= (a1 * |((x1 - x2),(x1 - x2))|) + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:26
.= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * |((x0 - x2),(x1 - x2))|) by EUCLID_4:26
.= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * (|((x0 - x1),(x1 - x2))| + |((x1 - x2),(x1 - x2))|)) by A18, EUCLID_4:25
.= (a1 + a3) * |((x1 - x2),(x1 - x2))| by A17 ;
x1 - x2 <> 0* n by A8, Th14;
then |((x1 - x2),(x1 - x2))| <> 0 by EUCLID_4:22;
then a1 + a3 = 0 by A19, XCMPLX_1:6;
then a3 = - a1 ;
then A20: x - x2 = a1 * ((x1 + (- x2)) - (x0 - x2)) by A14, Th17
.= a1 * ((x1 - x0) + ((- x2) - (- x2))) by Th23
.= a1 * ((x1 - x0) + (0* n)) by Th7
.= a1 * (x1 - x0) by EUCLID_4:1 ;
( x - x2 <> 0* n & x1 - x0 <> 0* n ) by A9, A10, Th14;
then A21: x - x2 // x1 - x0 by A20, Def1;
( L1 = Line x0,x1 & L2 = Line x2,x ) by A5, A6, A9, A10, Th69;
hence L1 // L2 by A21, Def7; :: thesis: verum

end;

end;

end;

hence L1 // L2 ; :: thesis: verum