let n be Nat; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n st L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st L is being_line holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L )
let L be Element of line_of_REAL n; :: thesis: ( L is being_line implies ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L ) )
assume L is being_line ; :: thesis: ex L0 being Element of line_of_REAL n st
( x in L0 & L0 // L )
then consider y0, y1 being Element of REAL n such that
A1: y0 <> y1 and
A2: L = Line (y0,y1) ;
set x9 = x + (y1 - y0);
reconsider L0 = Line (x,(x + (y1 - y0))) as Element of line_of_REAL n by Th47;
take L0 ; :: thesis: ( x in L0 & L0 // L )
A3: y1 - y0 <> 0* n by A1, Th9;
A4: (x + (y1 - y0)) - x = y1 - y0 by Th6;
then (x + (y1 - y0)) - x = 1 * (y1 - y0) by EUCLID_4:3;
then (x + (y1 - y0)) - x // y1 - y0 by A4, A3;
hence ( x in L0 & L0 // L ) by A2, EUCLID_4:9; :: thesis: verum