A9: p <> a by A4, DIRAF:31;
assume that
A10: b <> c and
A11: d <> a ; :: thesis: Mid p,d,a
assume not Mid p,d,a ; :: thesis: contradiction
then Mid p,a,d by A3, DIRAF:7;
then p,a // a,d by DIRAF:def 3;
then consider e1 being Element of OAS such that
A12: c,a // a,e1 and
A13: c,p // d,e1 by A9, ANALOAF:def 5;
A14: d,e1 // c,p by A13, DIRAF:2;
A15: c <> e1 by A12, DIRAF:def 3, A4, A6, DIRAF:8;
Mid b,c,p by A1, DIRAF:9;
then A16: b,c // c,p by DIRAF:def 3;
then A17: c,p // b,c by DIRAF:2;
consider e2 being Element of OAS such that
A18: b,a // a,e2 and
A19: b,c // e1,e2 by A4, A6, A12, ANALOAF:def 5;
consider e3 being Element of OAS such that
A20: b,c // e2,e3 and
A21: b,e2 // c,e3 and
c <> e3 by ANALOAF:def 5;
A22: a <> b by A4, DIRAF:31;
A23: Mid c,a,e1 by A12, DIRAF:def 3;
A24: d <> e1 b,a // b,e2 by A18, ANALOAF:def 5;
then A27: c,d // b,e2 by A2, A22, DIRAF:3;
b <> e2 by A22, A18, ANALOAF:def 5;
then c,d // c,e3 by A21, A27, DIRAF:3;
then ( Mid c,d,e3 or Mid c,e3,d ) by DIRAF:7;
then ( c,d,e3 are_collinear or c,e3,d are_collinear ) by DIRAF:28;
then A28: d,e3,c are_collinear by DIRAF:30;
e1,e2 // c,p by A10, A19, A16, ANALOAF:def 5;
then A29: e1,e2 // d,e1 by A5, A13, DIRAF:3;
then d,e1 // e1,e2 by DIRAF:2;
then A30: d,e1 // d,e2 by ANALOAF:def 5;
then d,e2 // d,e1 by DIRAF:2;
then d,e2 // c,p by A24, A14, DIRAF:3;
then d,e2 // b,c by A5, A17, DIRAF:3;
then A31: d,e2 // e2,e3 by A10, A20, DIRAF:3;
then Mid d,e2,e3 by DIRAF:def 3;
then d,e2,e3 are_collinear by DIRAF:28;
then A32: d,e3,e2 are_collinear by DIRAF:30;
A33: d <> e2 by A24, A29, ANALOAF:def 5;
then A34: d <> e3 by A31, ANALOAF:def 5;
d,e2 // d,e3 by A31, ANALOAF:def 5;
then d,e1 // d,e3 by A30, A33, DIRAF:3;
then ( Mid d,e1,e3 or Mid d,e3,e1 ) by DIRAF:7;
then ( d,e1,e3 are_collinear or d,e3,e1 are_collinear ) by DIRAF:28;
then A35: d,e3,e1 are_collinear by DIRAF:30;
c,a,e1 are_collinear by A23, DIRAF:28;
then c,e1,a are_collinear by DIRAF:30;
then A36: d,e3,a are_collinear by A15, A28, A35, DIRAF:35;
A37: a <> e1 A40: a <> e2 Mid b,a,e2 by A18, DIRAF:def 3;
then b,a,e2 are_collinear by DIRAF:28;
then a,e2,b are_collinear by DIRAF:30;
then A44: d,e3,b are_collinear by A40, A36, A32, DIRAF:35;
c,b,p are_collinear by A6, DIRAF:30;
then d,e3,p are_collinear by A10, A28, A44, DIRAF:35;
hence contradiction by A4, A34, A36, A44, DIRAF:32; :: thesis: verum

assume b = c ; :: thesis: a = d
then ( Mid b,d,a or Mid b,a,d ) by A2, DIRAF:7;
then ( b,d,a are_collinear or b,a,d are_collinear ) by DIRAF:28;
then A46: d,a,b are_collinear by DIRAF:30;
A47: d,a,a are_collinear by DIRAF:31;
d,a,p are_collinear by A45, DIRAF:30;
hence a = d by A4, A46, A47, DIRAF:32; :: thesis: verum