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 L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L )
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 L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L )
let L be Element of line_of_REAL n; :: thesis: ( not x in L & L is being_line implies ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L ) )
assume ( not x in L & L is being_line ) ; :: thesis: ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L )
then consider x1, x2 being Element of REAL n such that
A1: L = Line (x1,x2) and
A2: x - x1 _|_ x2 - x1 by Th54;
reconsider L0 = Line (x1,x) as Subset of (REAL n) ;
reconsider L0 = L0 as Element of line_of_REAL n by Th47;
( x1 in L0 & x1 in L ) by A1, EUCLID_4:9;
then A3: ( x in L0 & L0 meets L ) by Th49, EUCLID_4:9;
L0 _|_ L by A1, A2;
hence ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L & L0 meets L ) by A3; :: thesis: verum