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 x in L1 & x in L2 & L1 _|_ L2 holds
ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 )
let x be Element of REAL n; :: thesis: for L1, L2 being Element of line_of_REAL n st x in L1 & x in L2 & L1 _|_ L2 holds
ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 )
let L1, L2 be Element of line_of_REAL n; :: thesis: ( x in L1 & x in L2 & L1 _|_ L2 implies ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 ) )
assume A1: ( x in L1 & x in L2 & L1 _|_ L2 ) ; :: thesis: ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 )
then A2: L1 <> L2 by Th80;
( L1 is being_line & L2 is being_line ) by A1, Th72;
then consider x0 being Element of REAL n such that
A3: ( x0 in L1 & not x0 in L2 ) by A2, Th84;
thus ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 ) by A1, A3; :: thesis: verum