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 :: thesis: ( p <> q implies ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) )

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 Def7;
take x = x; :: thesis: ( a,x _|_ p,q & LIN p,q,x )
thus ( a,x _|_ p,q & LIN p,q,x ) by A2, Th61; :: thesis: verum

end;

now :: thesis: ( p = q implies ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) )

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, Th58;
hence ( a,x _|_ p,q & LIN p,q,x ) by Th58; :: thesis: verum

end;

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