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 <> 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 that
A1: not x in L and
A2: L is being_line ; :: thesis: ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L & L0 <> L )
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L ) by A2, Th72;
hence ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L & L0 <> L ) by A1; :: thesis: verum