let OAS be OAffinSpace; :: thesis: for a, b, c, d1, d2, p being Element of OAS st not p,a,b are_collinear & p,b,c are_collinear & p,a,d1 are_collinear & p,a,d2 are_collinear & a,b '||' c,d1 & a,b '||' c,d2 holds
d1 = d2
let a, b, c, d1, d2, p be Element of OAS; :: thesis: ( not p,a,b are_collinear & p,b,c are_collinear & p,a,d1 are_collinear & p,a,d2 are_collinear & a,b '||' c,d1 & a,b '||' c,d2 implies d1 = d2 )
assume that
A1: not p,a,b are_collinear and
A2: p,b,c are_collinear and
A3: p,a,d1 are_collinear and
A4: p,a,d2 are_collinear 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 :: thesis: ( p <> c implies not d1 <> d2 )
p,a,a are_collinear by DIRAF:31;
then A10: d1,d2,a are_collinear by A3, A4, A7, DIRAF:32;
A11: d1,d2,d1 are_collinear by DIRAF:31;
A12: p,c,b are_collinear by A2, DIRAF:30;
A13: d1,d2,d2 are_collinear by DIRAF:31;
A14: p,a,p are_collinear by DIRAF:31;
then A15: d1,d2,p are_collinear by A3, A4, A7, DIRAF:32;
c,d1 '||' c,d2 by A5, A6, A8, DIRAF:23;
then A16: c,d1,d2 are_collinear by DIRAF:def 5;
then A17: d1,d2,c are_collinear by DIRAF:30;
assume A18: p <> c ; :: thesis: not d1 <> d2
assume A19: d1 <> d2 ; :: thesis: contradiction
d1,d2,p are_collinear by A3, A4, A7, A14, DIRAF:32;
then A20: p,c,d1 are_collinear by A19, A17, A11, DIRAF:32;
d1,d2,c are_collinear by A16, DIRAF:30;
then p,c,d2 are_collinear by A19, A15, A13, DIRAF:32;
then d1,d2,b are_collinear by A18, A20, A12, DIRAF:32;
hence contradiction by A1, A19, A15, A10, DIRAF:32; :: thesis: verum
end;
A21: p,d2,a are_collinear by A4, DIRAF:30;
A22: p,d1,a are_collinear by A3, DIRAF:30;
now :: thesis: ( c = p implies d1 = d2 )
A23: p,d2,p are_collinear by DIRAF:31;
assume A24: c = p ; :: thesis: d1 = d2
then A25: p,d2 '||' a,b by A6, DIRAF:22;
A26: now :: thesis: not p <> d2
assume A27: p <> d2 ; :: thesis: contradiction
then p,d2,b are_collinear by A21, A25, DIRAF:33;
hence contradiction by A1, A21, A23, A27, DIRAF:32; :: thesis: verum
end;
A28: p,d1,p are_collinear by DIRAF:31;
A29: p,d1 '||' a,b by A5, A24, DIRAF:22;
now :: thesis: not p <> d1
assume A30: p <> d1 ; :: thesis: contradiction
then p,d1,b are_collinear 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