let MS be OrtAfPl; :: thesis: for o, c, c1, a, a1, a2 being Element of st not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 holds
a1 = a2
let o, c, c1, a, a1, a2 be Element of ; :: thesis: ( not LIN o,c,a & o <> c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 implies a1 = a2 )
assume that
A1: not LIN o,c,a and
A2: ( o <> c1 & o,c _|_ o,c1 ) and
A3: ( o,a _|_ o,a1 & o,a _|_ o,a2 ) and
A4: ( c,a _|_ c1,a1 & c,a _|_ c1,a2 ) ; :: thesis: a1 = a2
reconsider o' = o, a1' = a1, a2' = a2, c1' = c1 as Element of by ANALMETR:47;
assume A5: a1 <> a2 ; :: thesis: contradiction
o <> a by A1, Th1;
then o,a1 // o,a2 by A3, ANALMETR:85;
then o',a1' // o',a2' by ANALMETR:48;
then LIN o',a1',a2' by AFF_1:def 1;
then A6: LIN a1',a2',o' by AFF_1:15;
a <> c by A1, Th1;
then c1,a1 // c1,a2 by A4, ANALMETR:85;
then c1',a1' // c1',a2' by ANALMETR:48;
then LIN c1',a1',a2' by AFF_1:def 1;
then A7: LIN a1',a2',c1' by AFF_1:15;
LIN a1',a2',a2' by AFF_1:16;
then LIN o',c1',a2' by A5, A6, A7, AFF_1:17;
then o',c1' // o',a2' by AFF_1:def 1;
then o,c1 // o,a2 by ANALMETR:48;
then A8: o,c _|_ o,a2 by A2, ANALMETR:84;
LIN a1',a2',a1' by AFF_1:16;
then LIN o',c1',a1' by A5, A6, A7, AFF_1:17;
then o',c1' // o',a1' by AFF_1:def 1;
then o,c1 // o,a1 by ANALMETR:48;
then A9: o,c _|_ o,a1 by A2, ANALMETR:84;
( o <> a1 or o <> a2 ) by A5;
then o,c // o,a by A3, A9, A8, ANALMETR:85;
hence contradiction by A1, ANALMETR:def 11; :: thesis: verum