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 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 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 L2 & L1 _|_ L2 implies ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 ) )
assume that
A1: x in L2 and
A2: L1 _|_ L2 ; :: thesis: ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 )
( L1 is being_line & L2 is being_line ) by A2, Th72;
then ex x0 being Element of REAL n st
( x0 in L1 & not x0 in L2 ) by A2, Th80, Th84;
hence ex x0 being Element of REAL n st
( x <> x0 & x0 in L1 & not x0 in L2 ) by A1; :: thesis: verum