let OAS be OAffinSpace; :: thesis: for a, b, c, d1, d2 being Element of OAS 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 OAS; :: 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, DIRAF:37;
then A8: c,d1 '||' c,d2 by A2, A3, DIRAF:28;
b,d1 '||' b,d2 by A4, A5, A7, DIRAF:28;
then A9: ( LIN c,d1,d2 & LIN b,d1,d2 ) by A8, DIRAF:def 5;
then A10: ( LIN d1,d2,c & LIN d1,d2,b ) by DIRAF:36;
( LIN d1,d2,c & LIN d1,d2,d1 ) by A9, DIRAF:36, DIRAF:37;
then d1,d2 '||' c,d1 by DIRAF:40;
then A11: ( d1,d2 '||' a,b or c = d1 ) by A2, DIRAF:28;

now

assume c = d1 ; :: thesis: contradiction
then c,a '||' c,b by A4, DIRAF:27;
then LIN c,a,b by DIRAF:def 5;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

then d1,d2 '||' b,a by A11, DIRAF:27;
then LIN d1,d2,a by A6, A10, DIRAF:39;
hence contradiction by A1, A6, A10, DIRAF:38; :: thesis: verum