let OAS be OAffinSpace; :: thesis: for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds
ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
let a, b, c, d, x be Element of OAS; :: thesis: ( Mid a,b,d & Mid a,x,c & not a,b,c are_collinear implies ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) )
assume that
A1: Mid a,b,d and
A2: Mid a,x,c and
A3: not a,b,c are_collinear ; :: thesis: ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
A4: b <> c by A3, DIRAF:31;
A5: a <> b by A3, DIRAF:31;

A6: now :: thesis: ( b <> d & x <> c & a <> x implies ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) )

assume that
A7: b <> d and
A8: x <> c and
A9: a <> x ; :: thesis: ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
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, Th20;
A13: Mid e1,d,a by A11, DIRAF:9;
A14: d,b,a are_collinear by A1, DIRAF:9, DIRAF:28;
A15: not a,x,b are_collinear

proof

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

end;

A18: not x,d,a are_collinear

proof

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

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: c,b,e2 are_collinear 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 Th19;
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 :: thesis: not Mid x,d,y

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

proof

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

end;

c9,b,y are_collinear by A40, DIRAF:28;
then A45: b,y,c9 are_collinear by DIRAF:30;
then A46: c,c9,c are_collinear by A42, A35, DIRAF:32;
b,y,b are_collinear by DIRAF:31;
then A47: c,c9,b are_collinear by A42, A35, A45, DIRAF:32;
x,a,a are_collinear by DIRAF:31;
then c,c9,a are_collinear 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: verum

end;

A48: a <> e2

proof

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

end;

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

proof

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

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 :: thesis: Mid c,y,b

A55: b <> e2

proof

A56: a,b // b,d by A1, DIRAF:def 3;
assume A57: b = e2 ; :: thesis: contradiction
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 ( d,x,b are_collinear or d,b,x are_collinear ) by DIRAF:28;
then A58: d,b,x are_collinear by DIRAF:30;
d,b,b are_collinear by DIRAF:31;
then A59: a,x,b are_collinear by A7, A14, A58, DIRAF:32;
A60: a,x,c are_collinear by A2, DIRAF:28;
a,x,a are_collinear by A7, A14, A58, DIRAF:32;
hence contradiction by A3, A9, A59, A60, DIRAF:32; :: thesis: verum

end;

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

proof

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

end;

A65: b,e2,c are_collinear by A27, DIRAF:30;
assume A66: not Mid c,y,b ; :: thesis: contradiction
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, Th20;
A70: a,e2,a are_collinear by DIRAF:31;

A71: now :: thesis: not a = z

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

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 a,e2,z are_collinear by DIRAF:28;
then A73: a,z,e2 are_collinear by DIRAF:30;
A74: b,d,z are_collinear by A68, DIRAF:28;
then A75: a,z,a are_collinear by A7, A61, DIRAF:32;
b,d,b are_collinear by DIRAF:31;
then a,z,b are_collinear by A7, A74, A61, DIRAF:32;
then A76: a,e2,b are_collinear by A73, A75, A71, DIRAF:32;
a,e2,e2 are_collinear by A73, A75, A71, DIRAF:32;
then a,e2,c are_collinear by A55, A76, A65, DIRAF:35;
hence contradiction by A3, A48, A76, A70, DIRAF:32; :: thesis: verum

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: verum

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: verum