theorem Th81: :: EUCLIDLP:81

for n being Nat
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 )