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: ( LIN p,d1,a & LIN p,d2,a ) by A3, A4, DIRAF:36;
A8: ( p <> a & p <> b & a <> b ) by A1, DIRAF:37;

A9: now

assume c = p ; :: thesis: d1 = d2
then A10: ( p,d1 '||' a,b & p,d2 '||' a,b ) by A5, A6, DIRAF:27;
A11: ( LIN p,d1,p & LIN p,d2,p ) by DIRAF:37;

A12: now

assume A13: p <> d1 ; :: thesis: contradiction
then LIN p,d1,b by A7, A10, DIRAF:39;
hence contradiction by A1, A7, A11, A13, DIRAF:38; :: thesis: verum

end;

now

assume A14: p <> d2 ; :: thesis: contradiction
then LIN p,d2,b by A7, A10, DIRAF:39;
hence contradiction by A1, A7, A11, A14, DIRAF:38; :: thesis: verum

end;

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

end;

now

assume A15: p <> c ; :: thesis: not d1 <> d2
assume A16: d1 <> d2 ; :: thesis: contradiction
A17: LIN p,a,p by DIRAF:37;
then A18: LIN d1,d2,p by A3, A4, A8, DIRAF:38;
LIN p,a,a by DIRAF:37;
then A19: LIN d1,d2,a by A3, A4, A8, DIRAF:38;
c,d1 '||' c,d2 by A5, A6, A8, DIRAF:28;
then A20: LIN c,d1,d2 by DIRAF:def 5;
then A21: LIN d1,d2,c by DIRAF:36;
( LIN d1,d2,p & LIN d1,d2,c & LIN d1,d2,d1 ) by A3, A4, A8, A17, A20, DIRAF:36, DIRAF:38;
then A22: LIN p,c,d1 by A16, DIRAF:38;
LIN d1,d2,d2 by DIRAF:37;
then ( LIN p,c,d2 & LIN p,c,b ) by A2, A16, A18, A21, DIRAF:36, DIRAF:38;
then LIN d1,d2,b by A15, A22, DIRAF:38;
hence contradiction by A1, A16, A18, A19, DIRAF:38; :: thesis: verum

end;

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