theorem Th80: :: EUCLIDLP:80

for n being Nat
for x being Element of REAL n
for L1, L2 being Element of line_of_REAL n st L1 _|_ L2 holds
ex L0 being Element of line_of_REAL n st
( x in L0 & L0 _|_ L2 & L0 // L1 )