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