let n be 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 that
A1: L c= P and
A2: L1 c= P and
A3: L2 c= P ; :: thesis: ( not L _|_ L1 or not L _|_ L2 or L1 // L2 )
assume that
A4: L _|_ L1 and
A5: L _|_ L2 ; :: thesis: L1 // L2
L,L2 are_coplane by A1, A3, Th96;
then L meets L2 by A5, Th109;
then consider x2 being Element of REAL n such that
A6: x2 in L and
A7: x2 in L2 by Th49;
A8: L1 is being_line by A4, Th67;
L,L1 are_coplane by A1, A2, Th96;
then L meets L1 by A4, Th109;
then consider x1 being Element of REAL n such that
A9: x1 in L and
A10: x1 in L1 by Th49;
A11: L2 is being_line by A5, Th67;

now :: thesis: ( ( x1 = x2 & L1 // L2 ) or ( x1 <> x2 & L1 // L2 ) )

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

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

hence L1 // L2 by A1, A2, A3, A4, A5, A9, A10, A7, A8, Th65, Th108; :: thesis: verum

end;

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

then x1 - x2 <> 0* n by Th9;
then A13: |((x1 - x2),(x1 - x2))| <> 0 by EUCLID_4:17;
consider x being Element of REAL n such that
A14: x <> x2 and
A15: x in L2 by A11, Th53;
A16: L2 = Line (x2,x) by A7, A14, A15, Th64;
consider x0 being Element of REAL n such that
A17: x0 <> x1 and
A18: x0 in L1 by A8, Th53;
A19: L1 = Line (x0,x1) by A10, A17, A18, Th64;
A20: x0 - x1 _|_ x2 - x1 by A4, A9, A10, A6, A12, A17, A18, Th74;
then x0 - x1,x2 - x1 are_orthogonal ;
then A21: |((x0 - x1),(x2 - x1))| = 0 by RVSUM_1:def 17;
P = plane (x1,x0,x2) by A1, A2, A9, A6, A18, A20, Th45, Th92;
then consider a1, a3, a2 being Real such that
A22: (a1 + a3) + a2 = 1 and
A23: x = ((a1 * x1) + (a3 * x0)) + (a2 * x2) by A3, A15, Th88;
A24: (a2 + a1) + a3 = 1 by A22;
A25: x - x2 = (- x2) + (((a2 * x2) + (a1 * x1)) + (a3 * x0)) by A23, RVSUM_1:15
.= (- x2) + ((x2 + (a1 * (x1 - x2))) + (a3 * (x0 - x2))) by A24, Th27
.= (- x2) + (x2 + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))) by RVSUM_1:15
.= ((- x2) + x2) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by RVSUM_1:15
.= (0* n) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by Th2
.= (a1 * (x1 - x2)) + (a3 * (x0 - x2)) by EUCLID_4:1 ;
A26: |((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:22
.= 0 by A21 ;
A27: x0 - x2 = x0 - ((0* n) + x2) by EUCLID_4:1
.= x0 - ((x1 - x1) + x2) by Th2
.= (x0 - (x1 - x1)) - x2 by RVSUM_1:39
.= ((x0 - x1) + x1) - x2 by Th4
.= (x0 - x1) + (x1 - x2) by Th5 ;
x - x2 _|_ x1 - x2 by A5, A9, A6, A7, A12, A14, A15, Th74;
then x - x2,x1 - x2 are_orthogonal ;
then 0 = |(((a1 * (x1 - x2)) + (a3 * (x0 - x2))),(x1 - x2))| by A25, RVSUM_1:def 17
.= |((a1 * (x1 - x2)),(x1 - x2))| + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:20
.= (a1 * |((x1 - x2),(x1 - x2))|) + |((a3 * (x0 - x2)),(x1 - x2))| by EUCLID_4:21
.= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * |((x0 - x2),(x1 - x2))|) by EUCLID_4:21
.= (a1 * |((x1 - x2),(x1 - x2))|) + (a3 * (|((x0 - x1),(x1 - x2))| + |((x1 - x2),(x1 - x2))|)) by A27, EUCLID_4:20
.= (a1 + a3) * |((x1 - x2),(x1 - x2))| by A26 ;
then a1 + a3 = 0 by A13, XCMPLX_1:6;
then a3 = - a1 ;
then A28: x - x2 = a1 * ((x1 + (- x2)) - (x0 - x2)) by A25, Th12
.= a1 * ((x1 - x0) + ((- x2) - (- x2))) by Th18
.= a1 * ((x1 - x0) + (0* n)) by Th2
.= a1 * (x1 - x0) by EUCLID_4:1 ;
A29: x1 - x0 <> 0* n by A17, Th9;
x - x2 <> 0* n by A14, Th9;
then x - x2 // x1 - x0 by A28, A29;
hence L1 // L2 by A19, A16; :: thesis: verum

end;

end;

end;

hence L1 // L2 ; :: thesis: verum