let OAS be OAffinSpace; :: thesis: for a, b, c, p being Element of OAS st not p,a,b are_collinear & Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
let a, b, c, p be Element of OAS; :: thesis: ( not p,a,b are_collinear & Mid p,c,b implies ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) )
assume that
A1: not p,a,b are_collinear and
A2: Mid p,c,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
A3: p <> a by A1, DIRAF:31;
A4: p,c,b are_collinear by A2, DIRAF:28;
A5: Mid b,c,p by A2, DIRAF:9;
then A6: b,c // c,p by DIRAF:def 3;
A7: a <> b by A1, DIRAF:31;

A8: now :: thesis: ( b <> c & a <> c & p <> c implies ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) )

assume that
A9: b <> c and
A10: a <> c and
A11: p <> c ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
consider e1 being Element of OAS such that
A12: Mid b,e1,a and
A13: p,a // c,e1 by A5, Th19;
A14: not p,c,a are_collinear

proof

A15: p,c,p are_collinear by DIRAF:31;
assume p,c,a are_collinear ; :: thesis: contradiction
hence contradiction by A1, A4, A11, A15, DIRAF:32; :: thesis: verum

end;

A16: a <> e1

proof

assume a = e1 ; :: thesis: contradiction
then a,p // a,c by A13, DIRAF:2;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7;
then ( a,p,c are_collinear or a,c,p are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

consider e4 being Element of OAS such that
A17: e1,c // c,e4 and
A18: e1,b // p,e4 by A6, A9, ANALOAF:def 5;
consider e2 being Element of OAS such that
A19: a,c // c,e2 and
A20: a,b // p,e2 by A6, A9, ANALOAF:def 5;
consider e3 being Element of OAS such that
A21: p,c // c,e3 and
A22: p,a // e2,e3 by A10, A19, ANALOAF:def 5;
A23: not a,b,c are_collinear

proof

assume a,b,c are_collinear ; :: thesis: contradiction
then A24: b,c,a are_collinear by DIRAF:30;
A25: b,c,b are_collinear by DIRAF:31;
b,c,p are_collinear by A4, DIRAF:30;
hence contradiction by A1, A9, A24, A25, DIRAF:32; :: thesis: verum

end;

A26: c <> e2

proof

assume A27: c = e2 ; :: thesis: contradiction
p,c // c,b by A6, DIRAF:2;
then a,b // c,b by A11, A20, A27, DIRAF:3;
then b,a // b,c by DIRAF:2;
then ( Mid b,a,c or Mid b,c,a ) by DIRAF:7;
then ( b,a,c are_collinear or b,c,a are_collinear ) by DIRAF:28;
hence contradiction by A23, DIRAF:30; :: thesis: verum

end;

A28: e2 <> e3

proof

assume e2 = e3 ; :: thesis: contradiction
then c,e2 // p,c by A21, DIRAF:2;
then a,c // p,c by A19, A26, DIRAF:3;
then c,a // c,p by DIRAF:2;
then ( Mid c,a,p or Mid c,p,a ) by DIRAF:7;
then ( c,a,p are_collinear or c,p,a are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

A29: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then b,c,a are_collinear by A12, DIRAF:28;
hence contradiction by A23, DIRAF:30; :: thesis: verum

end;

A30: p <> e4

proof

assume p = e4 ; :: thesis: contradiction
then c,e1 // p,c by A17, DIRAF:2;
then p,a // p,c by A13, A29, DIRAF:3;
then ( Mid p,a,c or Mid p,c,a ) by DIRAF:7;
then ( p,a,c are_collinear or p,c,a are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

Mid e1,c,e4 by A17, DIRAF:def 3;
then Mid e4,c,e1 by DIRAF:9;
then A31: e4,c // c,e1 by DIRAF:def 3;
c,e1 // e2,e3 by A3, A13, A22, ANALOAF:def 5;
then A32: e4,c // e2,e3 by A29, A31, DIRAF:3;
A33: e2 <> e4

proof

assume e2 = e4 ; :: thesis: contradiction
then c,e2 // e1,c by A17, DIRAF:2;
then a,c // e1,c by A19, A26, DIRAF:3;
then c,e1 // c,a by DIRAF:2;
then p,a // c,a by A13, A29, DIRAF:3;
then a,p // a,c by DIRAF:2;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7;
then ( a,p,c are_collinear or a,c,p are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

A34: c <> e3

proof

assume c = e3 ; :: thesis: contradiction
then c,e2 // a,p by A22, DIRAF:2;
then a,c // a,p by A19, A26, DIRAF:3;
then ( Mid a,c,p or Mid a,p,c ) by DIRAF:7;
then ( a,c,p are_collinear or a,p,c are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

A35: p <> e3 by A11, A21, ANALOAF:def 5;
A36: not p,e3,e2 are_collinear

proof

p,c // c,b by A2, DIRAF:def 3;
then A37: p,c // p,b by ANALOAF:def 5;
p,c // p,e3 by A21, ANALOAF:def 5;
then p,b // p,e3 by A11, A37, ANALOAF:def 5;
then ( Mid p,b,e3 or Mid p,e3,b ) by DIRAF:7;
then ( p,b,e3 are_collinear or p,e3,b are_collinear ) by DIRAF:28;
then A38: p,e3,b are_collinear by DIRAF:30;
A39: p,e3,p are_collinear by DIRAF:31;
a,c // a,e2 by A19, ANALOAF:def 5;
then ( Mid a,c,e2 or Mid a,e2,c ) by DIRAF:7;
then ( a,c,e2 are_collinear or a,e2,c are_collinear ) by DIRAF:28;
then A40: c,e2,a are_collinear by DIRAF:30;
p,c // p,e3 by A21, ANALOAF:def 5;
then ( Mid p,c,e3 or Mid p,e3,c ) by DIRAF:7;
then ( p,c,e3 are_collinear or p,e3,c are_collinear ) by DIRAF:28;
then A41: p,e3,c are_collinear by DIRAF:30;
assume p,e3,e2 are_collinear ; :: thesis: contradiction
then p,e3,a are_collinear by A26, A41, A40, DIRAF:35;
hence contradiction by A1, A35, A38, A39, DIRAF:32; :: thesis: verum

end;

then A42: not e3,e2,p are_collinear by DIRAF:30;
consider e5 being Element of OAS such that
A43: e4,e2 // c,e5 and
A44: e4,c // e2,e5 and
A45: e2 <> e5 by ANALOAF:def 5;
A46: b <> e1

proof

p,c // c,b by A2, DIRAF:def 3;
then A47: c,b // p,c by DIRAF:2;
assume b = e1 ; :: thesis: contradiction
then p,a // p,c by A9, A13, A47, DIRAF:3;
then ( Mid p,a,c or Mid p,c,a ) by DIRAF:7;
then ( p,a,c are_collinear or p,c,a are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

A48: c <> e4

proof

assume A49: c = e4 ; :: thesis: contradiction
p,c // c,b by A2, DIRAF:def 3;
then e1,b // c,b by A11, A18, A49, DIRAF:3;
then b,e1 // b,c by DIRAF:2;
then ( Mid b,e1,c or Mid b,c,e1 ) by DIRAF:7;
then ( b,e1,c are_collinear or b,c,e1 are_collinear ) by DIRAF:28;
then A50: b,e1,c are_collinear by DIRAF:30;
A51: b,e1,b are_collinear by DIRAF:31;
b,e1,a are_collinear by A12, DIRAF:28;
hence contradiction by A23, A46, A50, A51, DIRAF:32; :: thesis: verum

end;

A52: c <> e5

proof

assume c = e5 ; :: thesis: contradiction
then c,e4 // c,e2 by A44, DIRAF:2;
then e1,c // c,e2 by A17, A48, DIRAF:3;
then c,e2 // e1,c by DIRAF:2;
then a,c // e1,c by A19, A26, DIRAF:3;
then c,e1 // c,a by DIRAF:2;
then p,a // c,a by A13, A29, DIRAF:3;
then a,p // a,c by DIRAF:2;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:7;
then ( a,p,c are_collinear or a,c,p are_collinear ) by DIRAF:28;
hence contradiction by A14, DIRAF:30; :: thesis: verum

end;

Mid a,e1,b by A12, DIRAF:9;
then A53: a,e1 // e1,b by DIRAF:def 3;
then a,e1 // a,b by ANALOAF:def 5;
then a,b // e1,b by A16, A53, ANALOAF:def 5;
then e1,b // p,e2 by A7, A20, ANALOAF:def 5;
then A54: p,e4 // p,e2 by A18, A46, ANALOAF:def 5;
Mid p,c,e3 by A21, DIRAF:def 3;
then Mid p,e4,e2 by A36, A32, A30, A54, Th16;
then A55: p,e4 // e4,e2 by DIRAF:def 3;
then p,e4 // p,e2 by ANALOAF:def 5;
then A56: p,e2 // e4,e2 by A30, A55, ANALOAF:def 5;
then A57: p,e2 // c,e5 by A43, A33, DIRAF:3;
p <> e2

proof

assume p = e2 ; :: thesis: contradiction
then Mid a,c,p by A19, DIRAF:def 3;
hence contradiction by A14, DIRAF:9, DIRAF:28; :: thesis: verum

end;

then A58: a,b // e4,e2 by A20, A56, DIRAF:3;
then A59: a,b // c,e5 by A43, A33, DIRAF:3;
A60: e5 <> e3

proof

assume e5 = e3 ; :: thesis: contradiction
then c,e3 // a,b by A59, DIRAF:2;
then p,c // a,b by A21, A34, DIRAF:3;
then c,p // b,a by DIRAF:2;
then b,c // b,a by A6, A11, DIRAF:3;
then ( Mid b,c,a or Mid b,a,c ) by DIRAF:7;
then ( b,c,a are_collinear or b,a,c are_collinear ) by DIRAF:28;
hence contradiction by A23, DIRAF:30; :: thesis: verum

end;

c,e1 // e4,c by A17, DIRAF:2;
then c,e1 // e2,e5 by A44, A48, DIRAF:3;
then p,a // e2,e5 by A13, A29, DIRAF:3;
then e2,e3 // e2,e5 by A3, A22, ANALOAF:def 5;
then ( Mid e2,e3,e5 or Mid e2,e5,e3 ) by DIRAF:7;
then ( e2,e3,e5 are_collinear or e2,e5,e3 are_collinear ) by DIRAF:28;
then A61: e2,e3,e5 are_collinear by DIRAF:30;
Mid p,c,e3 by A21, DIRAF:def 3;
then A62: Mid e3,c,p by DIRAF:9;
e3,c // c,p by A21, DIRAF:2;
then consider x being Element of OAS such that
A63: e5,c // c,x and
A64: e5,e3 // p,x by A34, ANALOAF:def 5;
A65: c,e5 // x,c by A63, DIRAF:2;
Mid p,c,e3 by A21, DIRAF:def 3;
then Mid e3,c,p by DIRAF:9;
then e3,c // c,p by DIRAF:def 3;
then e3,c // e3,p by ANALOAF:def 5;
then e3,p // e3,c by DIRAF:2;
then not Mid e2,e3,e5 by A60, A57, A42, Th17;
then ( Mid e3,e2,e5 or Mid e2,e5,e3 ) by A61, DIRAF:29;
then ( e3,e2 // e2,e5 or Mid e3,e5,e2 ) by DIRAF:9, DIRAF:def 3;
then ( e3,e2 // e3,e5 or e3,e5 // e5,e2 ) by ANALOAF:def 5, DIRAF:def 3;
then A66: e3,e5 // e3,e2 by ANALOAF:def 5, DIRAF:2;
c,e5 // p,e2 by A57, DIRAF:2;
then Mid e3,e5,e2 by A34, A42, A66, A62, Th15;
then Mid e2,e5,e3 by DIRAF:9;
then A67: e2,e5 // e5,e3 by DIRAF:def 3;
then e2,e5 // e2,e3 by ANALOAF:def 5;
then e2,e3 // e5,e3 by A45, A67, ANALOAF:def 5;
then p,a // e5,e3 by A22, A28, DIRAF:3;
then p,a // p,x by A64, A60, DIRAF:3;
then A68: p,x // p,a by DIRAF:2;
a,b // c,e5 by A43, A33, A58, DIRAF:3;
then A69: a,b // x,c by A52, A65, DIRAF:3;
then c,x // b,a by DIRAF:2;
hence ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) by A1, A2, A11, A69, A68, Th15; :: thesis: verum

end;

A70: ( a = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:4, DIRAF:10;
A71: ( p = c implies ( a,b // c,c & Mid p,c,a ) ) by DIRAF:4, DIRAF:10;
( b = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:1, DIRAF:10;
hence ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) by A8, A70, A71; :: thesis: verum