let POS be OrtAfPl; 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; ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
A1:
now ( p <> q implies ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) )assume
p <> q
;
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;
( a,x _|_ p,q & LIN p,q,x )thus
(
a,
x _|_ p,
q &
LIN p,
q,
x )
by A2, Th61;
verum end;
now ( p = q implies ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x ) )assume A3:
p = q
;
ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )take x =
a;
( 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;
verum end;
hence
ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
by A1; verum