for POS being OrtAfPl
for K being Subset of POS
for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )