theorem Th3: :: CONMETR:3

for X being OrtAfPl
for A being Subset of X
for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )