let MS be OrtAfPl; :: thesis: for o, a, a1, b, b1, c, c1 being Element of MS st o,a _|_ o,a1 & 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,a _|_ o,a1 & 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,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 ) and
A2: ( a,b _|_ a1,b1 & a,c _|_ a1,c1 ) and
A3: ( not o,c // o,a & not o,a // o,b ) and
A4: o = a1 ; :: thesis: b,c _|_ b1,c1
A5: o = b1

proof

assume o <> b1 ; :: thesis: contradiction
then a,b // o,b by A1, A2, A4, ANALMETR:85;
then b,a // b,o by ANALMETR:81;
then LIN b,a,o by ANALMETR:def 11;
then LIN o,a,b by Th4;
hence contradiction by A3, ANALMETR:def 11; :: thesis: verum

end;

o = c1

proof

assume o <> c1 ; :: thesis: contradiction
then a,c // o,c by A1, A2, A4, ANALMETR:85;
then c,a // c,o by ANALMETR:81;
then LIN c,a,o by ANALMETR:def 11;
then LIN o,c,a by Th4;
hence contradiction by A3, ANALMETR:def 11; :: thesis: verum

end;

hence b,c _|_ b1,c1 by A5, ANALMETR:80; :: thesis: verum