let OAS be OAffinSpace; :: thesis:
let a, b, d, x, c be Element of OAS; :: thesis:
assume that
A1: Mid a,b,d and
A2: Mid a,x,c and
A3: not LIN a,b,c ; :: thesis:
A4: b <> c by A3, DIRAF:31;
A5: a <> b by A3, DIRAF:31;

A6: now

assume that
A7: b <> d and
A8: x <> c and
A9: a <> x ; :: thesis:
A10: a <> d by A1, A7, DIRAF:8;
consider e1 being Element of OAS such that
A11: Mid a,d,e1 and
A12: x,d // c,e1 by A2, A9, Th27;
A13: Mid e1,d,a by A11, DIRAF:9;
A14: LIN d,b,a by A1, DIRAF:9, DIRAF:28;
A15: not LIN a,x,b

proof

A16: LIN a,x,a by DIRAF:31;
assume A17: LIN a,x,b ; :: thesis:
LIN a,x,c by A2, DIRAF:28;
hence contradiction by A3, A9, A17, A16, DIRAF:32; :: thesis:

end;

A18: not LIN x,d,a

proof

assume LIN x,d,a ; :: thesis:
then A19: LIN d,a,x by DIRAF:30;
A20: LIN d,a,a by DIRAF:31;
LIN d,a,b by A14, DIRAF:30;
hence contradiction by A10, A15, A19, A20, DIRAF:32; :: thesis:

end;

then A21: x <> d by DIRAF:31;
A22: Mid d,b,a by A1, DIRAF:9;
Mid b,d,e1 by A1, A11, DIRAF:11;
then Mid e1,d,b by DIRAF:9;
then Mid e1,b,a by A22, A13, DIRAF:12;
then A23: e1,b // b,a by DIRAF:def 3;
e1 <> b by A7, A22, A13, DIRAF:14;
then consider e2 being Element of OAS such that
A24: c,b // b,e2 and
A25: c,e1 // a,e2 by A23, ANALOAF:def 5;
A26: Mid c,b,e2 by A24, DIRAF:def 3;
then A27: LIN c,b,e2 by DIRAF:28;
Mid c,x,a by A2, DIRAF:9;
then consider y being Element of OAS such that
A28: Mid c,y,e2 and
A29: a,e2 // x,y by Th26;
A30: ( Mid c,b,y or Mid c,y,b ) by A26, A28, DIRAF:17;
A31: c <> e2 by A4, A24, ANALOAF:def 5;

A32: now

LIN c,b,e2 by A26, DIRAF:28;
then A33: LIN c,e2,b by DIRAF:30;
LIN c,y,e2 by A28, DIRAF:28;
then A34: LIN c,e2,y by DIRAF:30;
LIN c,e2,c by DIRAF:31;
then A35: LIN b,y,c by A31, A34, A33, DIRAF:32;
LIN a,x,c by A2, DIRAF:28;
then A36: LIN x,a,c by DIRAF:30;
A37: Mid c,x,a by A2, DIRAF:9;
assume A38: Mid x,d,y ; :: thesis:
then consider c9 being Element of OAS such that
A39: Mid x,c9,a and
A40: Mid c9,b,y by A22, A18, Th35;
LIN x,c9,a by A39, DIRAF:28;
then A41: LIN x,a,c9 by DIRAF:30;
A42: b <> y

proof

assume b = y ; :: thesis:
then LIN x,d,b by A38, DIRAF:28;
then A43: LIN d,b,x by DIRAF:30;
A44: LIN d,b,b by DIRAF:31;
LIN a,x,c by A2, DIRAF:28;
then LIN d,b,c by A9, A14, A43, DIRAF:35;
hence contradiction by A3, A7, A14, A44, DIRAF:32; :: thesis:

end;

LIN c9,b,y by A40, DIRAF:28;
then A45: LIN b,y,c9 by DIRAF:30;
then A46: LIN c,c9,c by A42, A35, DIRAF:32;
LIN b,y,b by DIRAF:31;
then A47: LIN c,c9,b by A42, A35, A45, DIRAF:32;
LIN x,a,a by DIRAF:31;
then LIN c,c9,a by A9, A36, A41, DIRAF:32;
then Mid x,c,a by A3, A39, A47, A46, DIRAF:32;
hence contradiction by A8, A37, DIRAF:14; :: thesis:

end;

A48: a <> e2

proof

assume a = e2 ; :: thesis:
then Mid c,b,a by A24, DIRAF:def 3;
hence contradiction by A3, DIRAF:9, DIRAF:28; :: thesis:

end;

A49: LIN e1,d,a by A11, DIRAF:9, DIRAF:28;
A50: c <> e1

proof

assume c = e1 ; :: thesis:
then A51: LIN d,a,c by A49, DIRAF:30;
A52: LIN d,a,a by DIRAF:31;
LIN d,a,b by A14, DIRAF:30;
hence contradiction by A3, A10, A51, A52, DIRAF:32; :: thesis:

end;

then x,d // a,e2 by A12, A25, DIRAF:3;
then x,d // x,y by A48, A29, DIRAF:3;
then A53: ( Mid x,d,y or Mid x,y,d ) by DIRAF:7;
then A54: Mid d,y,x by A32, DIRAF:9;

now

A55: b <> e2

proof

A56: a,b // b,d by A1, DIRAF:def 3;
assume A57: b = e2 ; :: thesis:
c,e1 // x,d by A12, DIRAF:2;
then a,b // x,d by A25, A50, A57, ANALOAF:def 5;
then x,d // b,d by A5, A56, ANALOAF:def 5;
then d,x // d,b by DIRAF:2;
then ( Mid d,x,b or Mid d,b,x ) by DIRAF:7;
then ( LIN d,x,b or LIN d,b,x ) by DIRAF:28;
then A58: LIN d,b,x by DIRAF:30;
LIN d,b,b by DIRAF:31;
then A59: LIN a,x,b by A7, A14, A58, DIRAF:32;
A60: LIN a,x,c by A2, DIRAF:28;
LIN a,x,a by A7, A14, A58, DIRAF:32;
hence contradiction by A3, A9, A59, A60, DIRAF:32; :: thesis:

end;

A61: LIN b,d,a by A14, DIRAF:30;
A62: y <> d

proof

A63: LIN c,e2,c by DIRAF:31;
A64: LIN c,e2,b by A27, DIRAF:30;
assume y = d ; :: thesis:
then LIN c,d,e2 by A28, DIRAF:28;
then LIN c,e2,d by DIRAF:30;
then LIN c,e2,a by A7, A14, A64, DIRAF:35;
hence contradiction by A3, A31, A64, A63, DIRAF:32; :: thesis:

end;

A65: LIN b,e2,c by A27, DIRAF:30;
assume A66: not Mid c,y,b ; :: thesis:
then A67: y <> b by DIRAF:10;
Mid b,y,e2 by A28, A30, A66, DIRAF:11;
then consider z being Element of OAS such that
A68: Mid b,d,z and
A69: y,d // e2,z by A67, Th27;
A70: LIN a,e2,a by DIRAF:31;

A71: now

assume A72: a = z ; :: thesis:
Mid d,b,a by A1, DIRAF:9;
hence contradiction by A7, A68, A72, DIRAF:14; :: thesis:

end;

d,y // y,x by A54, DIRAF:def 3;
then d,y // d,x by ANALOAF:def 5;
then y,d // x,d by DIRAF:2;
then y,d // c,e1 by A12, A21, DIRAF:3;
then c,e1 // e2,z by A69, A62, ANALOAF:def 5;
then a,e2 // e2,z by A25, A50, ANALOAF:def 5;
then Mid a,e2,z by DIRAF:def 3;
then LIN a,e2,z by DIRAF:28;
then A73: LIN a,z,e2 by DIRAF:30;
A74: LIN b,d,z by A68, DIRAF:28;
then A75: LIN a,z,a by A7, A61, DIRAF:32;
LIN b,d,b by DIRAF:31;
then LIN a,z,b by A7, A74, A61, DIRAF:32;
then A76: LIN a,e2,b by A73, A75, A71, DIRAF:32;
LIN a,e2,e2 by A73, A75, A71, DIRAF:32;
then LIN a,e2,c by A55, A76, A65, DIRAF:35;
hence contradiction by A3, A48, A76, A70, DIRAF:32; :: thesis:

end;

then Mid b,y,c by DIRAF:9;
hence ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) by A53, A32; :: thesis:

end;

A77: ( b = d implies ( Mid b,d,c & Mid x,d,d ) ) by DIRAF:10;
A78: ( x = c implies ( Mid b,c,c & Mid x,c,d ) ) by DIRAF:10;
( a = x implies ( Mid b,b,c & Mid x,b,d ) ) by A1, DIRAF:10;
hence ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) by A6, A77, A78; :: thesis: