let MS be OrtAfPl; for o, a, a1, b, b1, c, c1 being Element of MS st o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 holds
b,c _|_ b1,c1
let o, a, a1, b, b1, c, c1 be Element of MS; ( o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o = a1 implies b,c _|_ b1,c1 )
assume that
A1:
o,b _|_ o,b1
and
A2:
o,c _|_ o,c1
and
A3:
a,b _|_ a1,b1
and
A4:
a,c _|_ a1,c1
and
A5:
not o,c // o,a
and
A6:
not o,a // o,b
and
A7:
o = a1
; b,c _|_ b1,c1
A8:
o = c1
proof
assume
o <> c1
;
contradiction
then
a,
c // o,
c
by A2, A4, A7, ANALMETR:63;
then
c,
a // c,
o
by ANALMETR:59;
then
LIN c,
a,
o
by ANALMETR:def 10;
then
LIN o,
c,
a
by Th4;
hence
contradiction
by A5, ANALMETR:def 10;
verum
end;
o = b1
proof
assume
o <> b1
;
contradiction
then
a,
b // o,
b
by A1, A3, A7, ANALMETR:63;
then
b,
a // b,
o
by ANALMETR:59;
then
LIN b,
a,
o
by ANALMETR:def 10;
then
LIN o,
a,
b
by Th4;
hence
contradiction
by A6, ANALMETR:def 10;
verum
end;
hence
b,c _|_ b1,c1
by A8, ANALMETR:58; verum