let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds
L0 = L1
let x be Element of REAL n; :: thesis: for L0, L1, L2 being Element of line_of_REAL n
for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds
L0 = L1
let L0, L1, L2 be Element of line_of_REAL n; :: thesis: for P being Element of plane_of_REAL n st L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 holds
L0 = L1
let P be Element of plane_of_REAL n; :: thesis: ( L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 implies L0 = L1 )
assume A1: ( L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 ) ; :: thesis: ( not L0 _|_ L2 or not L1 _|_ L2 or L0 = L1 )
assume A2: ( L0 _|_ L2 & L1 _|_ L2 ) ; :: thesis: L0 = L1
then A3: ( L0 is being_line & L1 is being_line & L2 is being_line ) by Th72;
consider x0 being Element of REAL n such that
A4: ( x <> x0 & x0 in L0 & not x0 in L2 ) by A1, A2, Th86;
consider x2 being Element of REAL n such that
A5: ( x <> x2 & x2 in L2 & not x2 in L1 ) by A1, A2, Th86;
A6: L0 = Line x,x0 by A1, A4, Th69;
A7: x0 - x _|_ x2 - x by A1, A2, A4, A5, Th79;
then A8: P = plane x,x0,x2 by A1, A4, A5, Th50, Th97;
consider x1 being Element of REAL n such that
A9: ( x1 <> x & x1 in L1 ) by A1, A3, Th58;
consider a1, a2, a3 being Real such that
A10: ( (a1 + a2) + a3 = 1 & x1 = ((a1 * x) + (a2 * x0)) + (a3 * x2) ) by A1, A8, A9, Th93;
A11: x1 - x = (- x) + ((x + (a2 * (x0 - x))) + (a3 * (x2 - x))) by A10, Th32
.= (- x) + (x + ((a2 * (x0 - x)) + (a3 * (x2 - x)))) by RVSUM_1:32
.= ((- x) + x) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by RVSUM_1:32
.= (0* n) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by Th7
.= (a2 * (x0 - x)) + (a3 * (x2 - x)) by EUCLID_4:1 ;
A12: L1 = Line x,x1 by A1, A9, Th69;
A13: x1 - x _|_ x2 - x by A1, A2, A5, A9, Th79;
x0 - x,x2 - x are_orthogonal by A7, Def3;
then A14: |((x0 - x),(x2 - x))| = 0 by EUCLID_2:def 3;
A15: x1 - x,x2 - x are_orthogonal by A13, Def3;
x2 - x <> 0* n by A5, Th14;
then A16: |((x2 - x),(x2 - x))| <> 0 by EUCLID_4:22;
0 = |(((a2 * (x0 - x)) + (a3 * (x2 - x))),(x2 - x))| by A11, A15, EUCLID_2:def 3
.= |((a2 * (x0 - x)),(x2 - x))| + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:25
.= (a2 * |((x0 - x),(x2 - x))|) + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:26
.= a3 * |((x2 - x),(x2 - x))| by A14, EUCLID_4:26 ;
then A17: x1 - x = (a2 * (x0 - x)) + (0 * (x2 - x)) by A11, A16, XCMPLX_1:6
.= (a2 * (x0 - x)) + (0* n) by EUCLID_4:3
.= a2 * (x0 - x) by EUCLID_4:1 ;
( x1 - x <> 0* n & x0 - x <> 0* n ) by A4, A9, Th14;
then x1 - x // x0 - x by A17, Def1;
then A18: L1 // L0 by A6, A12, Def7;
L1 meets L0 by A1, Th54;
hence L0 = L1 by A18, Th76; :: thesis: verum