let AFS be AffinSpace; :: thesis: for a, b, c, d1, d2 being Element of AFS st not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 holds
d1 = d2
let a, b, c, d1, d2 be Element of AFS; :: thesis: ( not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 implies d1 = d2 )
assume that
A1: not LIN a,b,c and
A2: a,b // c,d1 and
A3: a,b // c,d2 and
A4: a,c // b,d1 and
A5: a,c // b,d2 ; :: thesis: d1 = d2
assume A6: d1 <> d2 ; :: thesis: contradiction
A7: ( a <> b & a <> c ) by A1, AFF_1:16;
then A8: c,d1 // c,d2 by A2, A3, AFF_1:14;
b,d1 // b,d2 by A4, A5, A7, AFF_1:14;
then A9: ( LIN c,d1,d2 & LIN b,d1,d2 ) by A8, AFF_1:def 1;
then A10: ( LIN d1,d2,c & LIN d1,d2,b ) by AFF_1:15;
( LIN d1,d2,c & LIN d1,d2,d1 ) by A9, AFF_1:15, AFF_1:16;
then d1,d2 // c,d1 by AFF_1:19;
then A11: ( d1,d2 // a,b or c = d1 ) by A2, AFF_1:14;

now

assume c = d1 ; :: thesis: contradiction
then c,a // c,b by A4, AFF_1:13;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A1, AFF_1:15; :: thesis: verum

end;

then d1,d2 // b,a by A11, AFF_1:13;
then LIN d1,d2,a by A6, A10, AFF_1:18;
hence contradiction by A1, A6, A10, AFF_1:17; :: thesis: verum