let n be 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 that
A1: L0 c= P and
A2: L1 c= P and
A3: L2 c= P and
A4: x in L0 and
A5: x in L1 and
A6: x in L2 ; :: thesis: ( not L0 _|_ L2 or not L1 _|_ L2 or L0 = L1 )
A7: L1 meets L0 by A4, A5, Th49;
assume that
A8: L0 _|_ L2 and
A9: L1 _|_ L2 ; :: thesis: L0 = L1
consider x0 being Element of REAL n such that
A10: x <> x0 and
A11: x0 in L0 and
not x0 in L2 by A6, A8, Th81;
L1 is being_line by A9, Th67;
then consider x1 being Element of REAL n such that
A12: x1 <> x and
A13: x1 in L1 by Th53;
consider x2 being Element of REAL n such that
A14: x <> x2 and
A15: x2 in L2 and
not x2 in L1 by A5, A9, Th81;
A16: x0 - x _|_ x2 - x by A4, A6, A8, A10, A11, A14, A15, Th74;
then P = plane (x,x0,x2) by A1, A3, A4, A11, A15, Th45, Th92;
then consider a1, a2, a3 being Real such that
A17: ( (a1 + a2) + a3 = 1 & x1 = ((a1 * x) + (a2 * x0)) + (a3 * x2) ) by A2, A13, Th88;
x0 - x,x2 - x are_orthogonal by A16;
then A18: |((x0 - x),(x2 - x))| = 0 by RVSUM_1:def 17;
A19: x1 - x = (- x) + ((x + (a2 * (x0 - x))) + (a3 * (x2 - x))) by A17, Th27
.= (- x) + (x + ((a2 * (x0 - x)) + (a3 * (x2 - x)))) by RVSUM_1:15
.= ((- x) + x) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by RVSUM_1:15
.= (0* n) + ((a2 * (x0 - x)) + (a3 * (x2 - x))) by Th2
.= (a2 * (x0 - x)) + (a3 * (x2 - x)) by EUCLID_4:1 ;
x2 - x <> 0* n by A14, Th9;
then A20: |((x2 - x),(x2 - x))| <> 0 by EUCLID_4:17;
x1 - x _|_ x2 - x by A5, A6, A9, A14, A15, A12, A13, Th74;
then x1 - x,x2 - x are_orthogonal ;
then 0 = |(((a2 * (x0 - x)) + (a3 * (x2 - x))),(x2 - x))| by A19, RVSUM_1:def 17
.= |((a2 * (x0 - x)),(x2 - x))| + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:20
.= (a2 * |((x0 - x),(x2 - x))|) + |((a3 * (x2 - x)),(x2 - x))| by EUCLID_4:21
.= a3 * |((x2 - x),(x2 - x))| by A18, EUCLID_4:21 ;
then A21: x1 - x = (a2 * (x0 - x)) + (0 * (x2 - x)) by A19, A20, XCMPLX_1:6
.= (a2 * (x0 - x)) + (0* n) by EUCLID_4:3
.= a2 * (x0 - x) by EUCLID_4:1 ;
A22: x0 - x <> 0* n by A10, Th9;
x1 - x <> 0* n by A12, Th9;
then A23: x1 - x // x0 - x by A21, A22;
A24: L1 = Line (x,x1) by A5, A12, A13, Th64;
L0 = Line (x,x0) by A4, A10, A11, Th64;
then L1 // L0 by A24, A23;
hence L0 = L1 by A7, Th71; :: thesis: verum