let OAS be OAffinSpace; :: thesis: for p, a, b, c, d1, d2 being Element of OAS st not LIN p,a,b & LIN p,b,c & LIN p,a,d1 & LIN p,a,d2 & a,b '||' c,d1 & a,b '||' c,d2 holds
d1 = d2
let p, a, b, c, d1, d2 be Element of OAS; :: thesis: ( not LIN p,a,b & LIN p,b,c & LIN p,a,d1 & LIN p,a,d2 & a,b '||' c,d1 & a,b '||' c,d2 implies d1 = d2 )
assume that
A1: not LIN p,a,b and
A2: LIN p,b,c and
A3: LIN p,a,d1 and
A4: LIN p,a,d2 and
A5: a,b '||' c,d1 and
A6: a,b '||' c,d2 ; :: thesis: d1 = d2
A7: p <> a by A1, DIRAF:31;
A8: a <> b by A1, DIRAF:31;

A9: now

LIN p,a,a by DIRAF:31;
then A10: LIN d1,d2,a by A3, A4, A7, DIRAF:32;
A11: LIN d1,d2,d1 by DIRAF:31;
A12: LIN p,c,b by A2, DIRAF:30;
A13: LIN d1,d2,d2 by DIRAF:31;
A14: LIN p,a,p by DIRAF:31;
then A15: LIN d1,d2,p by A3, A4, A7, DIRAF:32;
c,d1 '||' c,d2 by A5, A6, A8, DIRAF:23;
then A16: LIN c,d1,d2 by DIRAF:def 5;
then A17: LIN d1,d2,c by DIRAF:30;
assume A18: p <> c ; :: thesis: not d1 <> d2
assume A19: d1 <> d2 ; :: thesis: contradiction
LIN d1,d2,p by A3, A4, A7, A14, DIRAF:32;
then A20: LIN p,c,d1 by A19, A17, A11, DIRAF:32;
LIN d1,d2,c by A16, DIRAF:30;
then LIN p,c,d2 by A19, A15, A13, DIRAF:32;
then LIN d1,d2,b by A18, A20, A12, DIRAF:32;
hence contradiction by A1, A19, A15, A10, DIRAF:32; :: thesis: verum

end;

A21: LIN p,d2,a by A4, DIRAF:30;
A22: LIN p,d1,a by A3, DIRAF:30;

now

A23: LIN p,d2,p by DIRAF:31;
assume A24: c = p ; :: thesis: d1 = d2
then A25: p,d2 '||' a,b by A6, DIRAF:22;

A26: now

assume A27: p <> d2 ; :: thesis: contradiction
then LIN p,d2,b by A21, A25, DIRAF:33;
hence contradiction by A1, A21, A23, A27, DIRAF:32; :: thesis: verum

end;

A28: LIN p,d1,p by DIRAF:31;
A29: p,d1 '||' a,b by A5, A24, DIRAF:22;

now

assume A30: p <> d1 ; :: thesis: contradiction
then LIN p,d1,b by A22, A29, DIRAF:33;
hence contradiction by A1, A22, A28, A30, DIRAF:32; :: thesis: verum

end;

hence d1 = d2 by A26; :: thesis: verum

end;

hence d1 = d2 by A9; :: thesis: verum