let n be Element of 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 & L = Line y0,y1 ) by EUCLID_4:def 2;
set x' = x + (y1 - y0);
A2: (x + (y1 - y0)) - x = y1 - y0 by Th11;
then A3: (x + (y1 - y0)) - x = 1 * (y1 - y0) by EUCLID_4:3;
y1 - y0 <> 0* n by A1, Th14;
then A4: (x + (y1 - y0)) - x // y1 - y0 by A2, A3, Def1;
reconsider L0 = Line x,(x + (y1 - y0)) as Element of line_of_REAL n by Th52;
take L0 ; :: thesis: ( x in L0 & L0 // L )
thus ( x in L0 & L0 // L ) by A1, A4, Def7, EUCLID_4:10; :: thesis: verum