let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line x1,x2 & x - x1 _|_ x2 - x1 )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st not x in L & L is being_line holds
ex x1, x2 being Element of REAL n st
( L = Line x1,x2 & x - x1 _|_ x2 - x1 )
let L be Element of line_of_REAL n; :: thesis: ( not x in L & L is being_line implies ex x1, x2 being Element of REAL n st
( L = Line x1,x2 & x - x1 _|_ x2 - x1 ) )
assume A1: ( not x in L & L is being_line ) ; :: thesis: ex x1, x2 being Element of REAL n st
( L = Line x1,x2 & x - x1 _|_ x2 - x1 )
then consider y0, y1 being Element of REAL n such that
A2: ( y0 <> y1 & L = Line y0,y1 ) by EUCLID_4:def 2;
consider x1 being Element of REAL n such that
A3: ( x1 in Line y0,y1 & y0 - y1,x - x1 are_orthogonal ) by Th48;
A4: ( y0 - y1 <> 0* n & x - x1 <> 0* n ) by A1, A2, A3, Th14;
then A5: y0 - y1 _|_ x - x1 by A3, Def3;
consider x2 being Element of REAL n such that
A6: ( x1 <> x2 & x2 in L ) by A1, EUCLID_4:15;
A7: x2 - x1 <> 0* n by A6, Th14;
consider a being Real such that
A8: x2 - x1 = a * (y0 - y1) by A2, A3, A6, Th36;
A9: x2 - x1 // y0 - y1 by A4, A7, A8, Def1;
take x1 ; :: thesis: ex x2 being Element of REAL n st
( L = Line x1,x2 & x - x1 _|_ x2 - x1 )
take x2 ; :: thesis: ( L = Line x1,x2 & x - x1 _|_ x2 - x1 )
thus ( L = Line x1,x2 & x - x1 _|_ x2 - x1 ) by A1, A2, A3, A5, A6, A9, Th35, Th49; :: thesis: verum