let MS be OrtAfPl; for a, b, c, d1, d2 being Element of st not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds
d1 = d2
let a, b, c, d1, d2 be Element of ; ( not LIN a,b,c & d1,a _|_ b,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c implies d1 = d2 )
assume that
A1:
not LIN a,b,c
and
A2:
d1,a _|_ b,c
and
A3:
d1,b _|_ a,c
and
A4:
d2,a _|_ b,c
and
A5:
d2,b _|_ a,c
; d1 = d2
reconsider a' = a, b' = b, c' = c, d1' = d1, d2' = d2 as Element of by ANALMETR:47;
assume A6:
d1 <> d2
; contradiction
b <> c
by A1, Th1;
then
d1,a // d2,a
by A2, A4, ANALMETR:85;
then
d1',a' // d2',a'
by ANALMETR:48;
then
a',d1' // a',d2'
by AFF_1:13;
then
LIN a',d1',d2'
by AFF_1:def 1;
then A7:
LIN d1',d2',a'
by AFF_1:15;
a <> c
by A1, Th1;
then
d1,b // d2,b
by A3, A5, ANALMETR:85;
then
d1',b' // d2',b'
by ANALMETR:48;
then
b',d1' // b',d2'
by AFF_1:13;
then
LIN b',d1',d2'
by AFF_1:def 1;
then A8:
LIN d1',d2',b'
by AFF_1:15;
set X' = Line a',b';
reconsider X = Line a',b' as Subset of by ANALMETR:57;
A9:
b <> a
by A1, Th1;
then A10:
Line a',b' is being_line
by AFF_1:def 3;
then A11:
X is being_line
by ANALMETR:58;
A12:
a' in Line a',b'
by AFF_1:26;
A13:
b' in Line a',b'
by AFF_1:26;
LIN d1',d2',d2'
by AFF_1:16;
then A14:
d2 in X
by A6, A9, A7, A8, A10, A12, A13, AFF_1:17, AFF_1:39;
LIN d1',d2',d1'
by AFF_1:16;
then A15:
d1 in X
by A6, A9, A7, A8, A10, A12, A13, AFF_1:17, AFF_1:39;
( a <> d1 or a <> d2 )
by A6;
then A16:
b,c _|_ X
by A2, A4, A12, A15, A14, A11, ANALMETR:77;
( b <> d1 or b <> d2 )
by A6;
then
a,c _|_ X
by A3, A5, A13, A15, A14, A11, ANALMETR:77;
then
a,c // b,c
by A16, Th2;
then
a',c' // b',c'
by ANALMETR:48;
then
c',b' // c',a'
by AFF_1:13;
then
LIN c',b',a'
by AFF_1:def 1;
then
LIN a',b',c'
by AFF_1:15;
hence
contradiction
by A1, ANALMETR:55; verum