let MS be OrtAfPl; :: thesis: 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; :: thesis: ( 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 ; :: thesis: b,c _|_ b1,c1
A8: o = c1

proof

assume o <> c1 ; :: thesis: 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; :: thesis: verum

end;

o = b1

proof

assume o <> b1 ; :: thesis: 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; :: thesis: verum

end;

hence b,c _|_ b1,c1 by A8, ANALMETR:58; :: thesis: verum