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
a <> c by A1, DIRAF:37;
then b,d1 '||' b,d2 by A4, A5, DIRAF:28;
then LIN b,d1,d2 by DIRAF:def 5;
then A7: LIN d1,d2,b by DIRAF:36;

A8: 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;

A9: LIN d1,d2,d1 by DIRAF:37;
a <> b by A1, DIRAF:37;
then c,d1 '||' c,d2 by A2, A3, DIRAF:28;
then A10: LIN c,d1,d2 by DIRAF:def 5;
then A11: LIN d1,d2,c by DIRAF:36;
LIN d1,d2,c by A10, DIRAF:36;
then d1,d2 '||' c,d1 by A9, DIRAF:40;
then ( d1,d2 '||' a,b or c = d1 ) by A2, DIRAF:28;
then d1,d2 '||' b,a by A8, DIRAF:27;
then LIN d1,d2,a by A6, A7, DIRAF:39;
hence contradiction by A1, A6, A11, A7, DIRAF:38; :: thesis: verum