let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & x in L2 holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )
let x be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 & x in L2 holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( L1 _|_ L2 & x in L2 implies ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 ) )
assume A1: ( L1 _|_ L2 & x in L2 ) ; :: thesis: ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )
then ( L1 is being_line & L2 is being_line ) by Th72;
then consider L0 being Element of line_of_REAL n such that
A2: ( x in L0 & L0 // L1 ) by Th77;
take L0 ; :: thesis: ( x in L0 & L0 _|_ L2 & L0 // L1 )
thus ( x in L0 & L0 _|_ L2 & L0 // L1 ) by A1, A2, Th66; :: thesis: verum