theorem :: ANALMETR:47

for POS being OrtAfSp
for K being Subset of POS
for a being Element of POS st K is being_line holds
a,a _|_ K