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 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 o9 = o, a19 = a1, a29 = a2, c19 = c1 as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
assume A5: a1 <> a2 ; :: thesis: contradiction
o <> a by A1, Th1;
then o,a1 // o,a2 by A3, ANALMETR:63;
then o9,a19 // o9,a29 by ANALMETR:36;
then LIN o9,a19,a29 by AFF_1:def 1;
then A6: LIN a19,a29,o9 by AFF_1:6;
a <> c by A1, Th1;
then c1,a1 // c1,a2 by A4, ANALMETR:63;
then c19,a19 // c19,a29 by ANALMETR:36;
then LIN c19,a19,a29 by AFF_1:def 1;
then A7: LIN a19,a29,c19 by AFF_1:6;
LIN a19,a29,a29 by AFF_1:7;
then LIN o9,c19,a29 by A5, A6, A7, AFF_1:8;
then o9,c19 // o9,a29 by AFF_1:def 1;
then o,c1 // o,a2 by ANALMETR:36;
then A8: o,c _|_ o,a2 by A2, ANALMETR:62;
LIN a19,a29,a19 by AFF_1:7;
then LIN o9,c19,a19 by A5, A6, A7, AFF_1:8;
then o9,c19 // o9,a19 by AFF_1:def 1;
then o,c1 // o,a1 by ANALMETR:36;
then A9: o,c _|_ o,a1 by A2, ANALMETR:62;
( o <> a1 or o <> a2 ) by A5;
then o,c // o,a by A3, A9, A8, ANALMETR:63;
hence contradiction by A1, ANALMETR:def 10; :: thesis: verum