let n be 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 that
A1: not x in L and
A2: L is being_line ; :: thesis: ex x1, x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1 _|_ x2 - x1 )
consider y0, y1 being Element of REAL n such that
A3: y0 <> y1 and
A4: L = Line (y0,y1) by A2;
A5: y0 - y1 <> 0* n by A3, Th9;
consider x1 being Element of REAL n such that
A6: x1 in Line (y0,y1) and
A7: y0 - y1,x - x1 are_orthogonal by Th43;
x - x1 <> 0* n by A1, A4, A6, Th9;
then A8: y0 - y1 _|_ x - x1 by A7, A5;
take x1 ; :: thesis: ex x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1 _|_ x2 - x1 )
consider x2 being Element of REAL n such that
A9: x1 <> x2 and
A10: x2 in L by A2, EUCLID_4:14;
take x2 ; :: thesis: ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 )
A11: x2 - x1 <> 0* n by A9, Th9;
ex a being Real st x2 - x1 = a * (y0 - y1) by A4, A6, A10, Th31;
then x2 - x1 // y0 - y1 by A5, A11;
hence ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) by A2, A4, A6, A8, A9, A10, Th30, Th44; :: thesis: verum