let MS be OrtAfPl; :: thesis: for a, b, c, d1, d2 being Element of MS 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 MS; :: thesis: ( 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 ; :: thesis: d1 = d2
reconsider a9 = a, b9 = b, c9 = c, d19 = d1, d29 = d2 as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
assume A6: d1 <> d2 ; :: thesis: contradiction
b <> c by A1, Th1;
then d1,a // d2,a by A2, A4, ANALMETR:63;
then d19,a9 // d29,a9 by ANALMETR:36;
then a9,d19 // a9,d29 by AFF_1:4;
then LIN a9,d19,d29 by AFF_1:def 1;
then A7: LIN d19,d29,a9 by AFF_1:6;
a <> c by A1, Th1;
then d1,b // d2,b by A3, A5, ANALMETR:63;
then d19,b9 // d29,b9 by ANALMETR:36;
then b9,d19 // b9,d29 by AFF_1:4;
then LIN b9,d19,d29 by AFF_1:def 1;
then A8: LIN d19,d29,b9 by AFF_1:6;
set X9 = Line (a9,b9);
reconsider X = Line (a9,b9) as Subset of MS ;
A9: b <> a by A1, Th1;
then A10: Line (a9,b9) is being_line by AFF_1:def 3;
then A11: X is being_line by ANALMETR:43;
A12: a9 in Line (a9,b9) by AFF_1:15;
A13: b9 in Line (a9,b9) by AFF_1:15;
LIN d19,d29,d29 by AFF_1:7;
then A14: d2 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1:8, AFF_1:25;
LIN d19,d29,d19 by AFF_1:7;
then A15: d1 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1:8, AFF_1:25;
( a <> d1 or a <> d2 ) by A6;
then A16: b,c _|_ X by A2, A4, A12, A15, A14, A11, ANALMETR:55;
( b <> d1 or b <> d2 ) by A6;
then a,c _|_ X by A3, A5, A13, A15, A14, A11, ANALMETR:55;
then a,c // b,c by A16, Th2;
then a9,c9 // b9,c9 by ANALMETR:36;
then c9,b9 // c9,a9 by AFF_1:4;
then LIN c9,b9,a9 by AFF_1:def 1;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A1, ANALMETR:40; :: thesis: verum