let MS be OrtAfPl; 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; ( 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 )
; 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
; 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; verum