let POS be OrtAfPl; :: thesis: for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
let a, p, q be Element of POS; :: thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )

A1: now

assume p <> q ; :: thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
then consider x being Element of POS such that
A2: ( p,q // p,x & p,q _|_ x,a ) by Def9;
take x = x; :: thesis: ( a,x _|_ p,q & LIN p,q,x )
thus ( a,x _|_ p,q & LIN p,q,x ) by A2, Def11, Th83; :: thesis: verum

end;

now

assume A3: p = q ; :: thesis: ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
take x = a; :: thesis: ( a,x _|_ p,q & LIN p,q,x )
p,q // p,a by A3, Th80;
hence ( a,x _|_ p,q & LIN p,q,x ) by Def11, Th80; :: thesis: verum

end;

hence ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) by A1; :: thesis: verum