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 & d1,b _|_ a,c ) and
A3: ( d2,a _|_ b,c & d2,b _|_ a,c ) ; :: thesis: d1 = d2
assume A4: d1 <> d2 ; :: thesis: contradiction
A5: ( a <> c & b <> a & b <> c ) by A1, Th1;
then A6: ( d1,a // d2,a & d1,b // d2,b ) by A2, A3, ANALMETR:85;
reconsider a' = a, b' = b, c' = c, d1' = d1, d2' = d2 as Element of (Af MS) by ANALMETR:47;
( d1',a' // d2',a' & d1',b' // d2',b' ) by A6, ANALMETR:48;
then ( a',d1' // a',d2' & b',d1' // b',d2' ) by AFF_1:13;
then ( LIN a',d1',d2' & LIN b',d1',d2' ) by AFF_1:def 1;
then A7: ( LIN d1',d2',a' & LIN d1',d2',b' ) by AFF_1:15;
( LIN d1',d2',d1' & LIN d1',d2',d2' ) by AFF_1:16;
then A8: ( LIN a',b',d1' & LIN a',b',d2' ) by A4, A7, AFF_1:17;
set X' = Line a',b';
A9: ( Line a',b' is being_line & a' in Line a',b' & b' in Line a',b' ) by A5, AFF_1:26, AFF_1:def 3;
reconsider X = Line a',b' as Subset of MS by ANALMETR:57;
A10: ( d1 in X & d2 in X & a in X & b in X & X is being_line ) by A5, A8, A9, AFF_1:39, ANALMETR:58;
( ( a <> d1 or a <> d2 ) & ( b <> d1 or b <> d2 ) ) by A4;
then ( a,c _|_ X & b,c _|_ X ) by A2, A3, A10, ANALMETR:77;
then a,c // b,c by 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; :: thesis: verum