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 are_lindependent2 )
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 are_lindependent2 )
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 are_lindependent2 ) )
assume ( 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 are_lindependent2 )
then consider x1, x2 being Element of REAL n such that
A1: ( L = Line (x1,x2) & x - x1 _|_ x2 - x1 ) by Th54;
take x1 ; :: thesis: ex x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
take x2 ; :: thesis: ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
thus ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 ) by A1, Th45; :: thesis: verum