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 L0 being Element of line_of_REAL n st
( x in L0 & L0 // L & L0 <> 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 <> 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 <> L ) )
assume A1: ( 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 <> L )
then consider L0 being Element of line_of_REAL n such that
A2: ( x in L0 & L0 // L ) by Th77;
thus ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L & L0 <> L ) by A1, A2; :: thesis: verum