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
a <> c by A1, AFF_1:7;
then b,d1 // b,d2 by A4, A5, AFF_1:5;
then LIN b,d1,d2 by AFF_1:def 1;
then A7: LIN d1,d2,b by AFF_1:6;
A8: now :: thesis: not c = d1
assume c = d1 ; :: thesis: contradiction
then c,a // c,b by A4, AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A1, AFF_1:6; :: thesis: verum
end;
A9: LIN d1,d2,d1 by AFF_1:7;
a <> b by A1, AFF_1:7;
then c,d1 // c,d2 by A2, A3, AFF_1:5;
then A10: LIN c,d1,d2 by AFF_1:def 1;
then A11: LIN d1,d2,c by AFF_1:6;
LIN d1,d2,c by A10, AFF_1:6;
then d1,d2 // c,d1 by A9, AFF_1:10;
then ( d1,d2 // a,b or c = d1 ) by A2, AFF_1:5;
then d1,d2 // b,a by A8, AFF_1:4;
then LIN d1,d2,a by A6, A7, AFF_1:9;
hence contradiction by A1, A6, A11, A7, AFF_1:8; :: thesis: verum