let n be Nat; 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; 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; ( 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 )
; 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
; ex x2 being Element of REAL n st
( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
take
x2
; ( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
thus
( L = Line (x1,x2) & x - x1,x2 - x1 are_lindependent2 )
by A1, Th45; verum