for POS being OrtAfPl
for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )