let OAS be OAffinSpace; :: thesis: for p, a, b, c being Element of OAS st not LIN p,a,b & Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
let p, a, b, c be Element of OAS; :: thesis: ( not LIN p,a,b & Mid p,c,b implies ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) )
assume that
A1: not LIN p,a,b 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 & p <> b & a <> b ) by A1, DIRAF:37;
A4: LIN p,c,b by A2, DIRAF:34;
A5: Mid b,c,p by A2, DIRAF:13;
then A6: b,c // c,p by DIRAF:def 3;

A7: now

assume A8: ( b <> c & a <> c & 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
A9: ( Mid b,e1,a & p,a // c,e1 ) by A5, Th26;
consider e2 being Element of OAS such that
A10: ( a,c // c,e2 & a,b // p,e2 ) by A6, A8, ANALOAF:def 5;
consider e3 being Element of OAS such that
A11: ( p,c // c,e3 & p,a // e2,e3 ) by A8, A10, ANALOAF:def 5;
consider e4 being Element of OAS such that
A12: ( e1,c // c,e4 & e1,b // p,e4 ) by A6, A8, ANALOAF:def 5;
consider e5 being Element of OAS such that
A13: ( e4,e2 // c,e5 & e4,c // e2,e5 & e2 <> e5 ) by ANALOAF:def 5;
A14: e3,c // c,p by A11, DIRAF:5;
A15: not LIN p,c,a

proof

assume LIN p,c,a ; :: thesis: contradiction
then ( LIN p,c,a & LIN p,c,p ) by DIRAF:37;
hence contradiction by A1, A4, A8, DIRAF:38; :: thesis: verum

end;

A16: not LIN a,b,c

proof

assume LIN a,b,c ; :: thesis: contradiction
then ( LIN b,c,a & LIN b,c,p & LIN b,c,b ) by A4, DIRAF:36, DIRAF:37;
hence contradiction by A1, A8, DIRAF:38; :: thesis: verum

end;

A17: p <> e2

proof

assume p = e2 ; :: thesis: contradiction
then Mid a,c,p by A10, DIRAF:def 3;
hence contradiction by A15, DIRAF:13, DIRAF:34; :: thesis: verum

end;

A18: c <> e2

proof

assume A19: c = e2 ; :: thesis: contradiction
p,c // c,b by A6, DIRAF:5;
then a,b // c,b by A8, A10, A19, DIRAF:6;
then b,a // b,c by DIRAF:5;
then ( Mid b,a,c or Mid b,c,a ) by DIRAF:11;
then ( LIN b,a,c or LIN b,c,a ) by DIRAF:34;
hence contradiction by A16, DIRAF:36; :: thesis: verum

end;

A20: c <> e3

proof

assume c = e3 ; :: thesis: contradiction
then c,e2 // a,p by A11, DIRAF:5;
then a,c // a,p by A10, A18, DIRAF:6;
then ( Mid a,c,p or Mid a,p,c ) by DIRAF:11;
then ( LIN a,c,p or LIN a,p,c ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

then consider x being Element of OAS such that
A21: ( e5,c // c,x & e5,e3 // p,x ) by A14, ANALOAF:def 5;
A22: p <> e3 by A8, A11, ANALOAF:def 5;
A23: not LIN p,e3,e2

proof

assume A24: LIN p,e3,e2 ; :: thesis: contradiction
p,c // p,e3 by A11, ANALOAF:def 5;
then ( Mid p,c,e3 or Mid p,e3,c ) by DIRAF:11;
then ( LIN p,c,e3 or LIN p,e3,c ) by DIRAF:34;
then A25: LIN p,e3,c by DIRAF:36;
a,c // a,e2 by A10, ANALOAF:def 5;
then ( Mid a,c,e2 or Mid a,e2,c ) by DIRAF:11;
then ( LIN a,c,e2 or LIN a,e2,c ) by DIRAF:34;
then LIN c,e2,a by DIRAF:36;
then A26: LIN p,e3,a by A18, A24, A25, DIRAF:41;
p,c // c,b by A2, DIRAF:def 3;
then ( p,c // p,b & p,c // p,e3 ) by A11, ANALOAF:def 5;
then p,b // p,e3 by A8, ANALOAF:def 5;
then ( Mid p,b,e3 or Mid p,e3,b ) by DIRAF:11;
then ( LIN p,b,e3 or LIN p,e3,b ) by DIRAF:34;
then ( LIN p,e3,b & LIN p,e3,p ) by DIRAF:36, DIRAF:37;
hence contradiction by A1, A22, A26, DIRAF:38; :: thesis: verum

end;

A27: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then LIN b,c,a by A9, DIRAF:34;
hence contradiction by A16, DIRAF:36; :: thesis: verum

end;

A28: e4,c // e2,e3

proof

A29: c,e1 // e2,e3 by A3, A9, A11, ANALOAF:def 5;
Mid e1,c,e4 by A12, DIRAF:def 3;
then Mid e4,c,e1 by DIRAF:13;
then e4,c // c,e1 by DIRAF:def 3;
hence e4,c // e2,e3 by A27, A29, DIRAF:6; :: thesis: verum

end;

A30: b <> e1

proof

assume b = e1 ; :: thesis: contradiction
then ( p,a // c,b & p,c // c,b ) by A2, A9, DIRAF:def 3;
then ( p,a // c,b & c,b // p,c ) by DIRAF:5;
then p,a // p,c by A8, DIRAF:6;
then ( Mid p,a,c or Mid p,c,a ) by DIRAF:11;
then ( LIN p,a,c or LIN p,c,a ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

A31: p <> e4

proof

assume p = e4 ; :: thesis: contradiction
then c,e1 // p,c by A12, DIRAF:5;
then p,a // p,c by A9, A27, DIRAF:6;
then ( Mid p,a,c or Mid p,c,a ) by DIRAF:11;
then ( LIN p,a,c or LIN p,c,a ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

A32: e2 <> e4

proof

assume e2 = e4 ; :: thesis: contradiction
then c,e2 // e1,c by A12, DIRAF:5;
then a,c // e1,c by A10, A18, DIRAF:6;
then c,e1 // c,a by DIRAF:5;
then p,a // c,a by A9, A27, DIRAF:6;
then a,p // a,c by DIRAF:5;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:11;
then ( LIN a,p,c or LIN a,c,p ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

A33: c <> e4

proof

assume c = e4 ; :: thesis: contradiction
then ( e1,b // p,c & p,c // c,b ) by A2, A12, DIRAF:def 3;
then e1,b // c,b by A8, DIRAF:6;
then b,e1 // b,c by DIRAF:5;
then ( Mid b,e1,c or Mid b,c,e1 ) by DIRAF:11;
then ( LIN b,e1,c or LIN b,c,e1 ) by DIRAF:34;
then ( LIN b,e1,c & LIN b,e1,a & LIN b,e1,b ) by A9, DIRAF:34, DIRAF:36, DIRAF:37;
hence contradiction by A16, A30, DIRAF:38; :: thesis: verum

end;

A34: c <> e5

proof

assume c = e5 ; :: thesis: contradiction
then c,e4 // c,e2 by A13, DIRAF:5;
then e1,c // c,e2 by A12, A33, DIRAF:6;
then c,e2 // e1,c by DIRAF:5;
then a,c // e1,c by A10, A18, DIRAF:6;
then c,e1 // c,a by DIRAF:5;
then p,a // c,a by A9, A27, DIRAF:6;
then a,p // a,c by DIRAF:5;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:11;
then ( LIN a,p,c or LIN a,c,p ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

A35: a <> e1

proof

assume a = e1 ; :: thesis: contradiction
then a,p // a,c by A9, DIRAF:5;
then ( Mid a,p,c or Mid a,c,p ) by DIRAF:11;
then ( LIN a,p,c or LIN a,c,p ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

Mid a,e1,b by A9, DIRAF:13;
then a,e1 // e1,b by DIRAF:def 3;
then ( a,e1 // e1,b & a,e1 // a,b ) by ANALOAF:def 5;
then a,b // e1,b by A35, ANALOAF:def 5;
then e1,b // p,e2 by A3, A10, ANALOAF:def 5;
then A36: p,e4 // p,e2 by A12, A30, ANALOAF:def 5;
Mid p,c,e3 by A11, DIRAF:def 3;
then Mid p,e4,e2 by A23, A28, A31, A36, Th23;
then p,e4 // e4,e2 by DIRAF:def 3;
then ( p,e4 // e4,e2 & p,e4 // p,e2 ) by ANALOAF:def 5;
then A37: p,e2 // e4,e2 by A31, ANALOAF:def 5;
then A38: a,b // e4,e2 by A10, A17, DIRAF:6;
then A39: a,b // c,e5 by A13, A32, DIRAF:6;
( a,b // c,e5 & c,e5 // x,c ) by A13, A21, A32, A38, DIRAF:5, DIRAF:6;
then A40: a,b // x,c by A34, DIRAF:6;
A41: e2 <> e3

proof

assume e2 = e3 ; :: thesis: contradiction
then c,e2 // p,c by A11, DIRAF:5;
then a,c // p,c by A10, A18, DIRAF:6;
then c,a // c,p by DIRAF:5;
then ( Mid c,a,p or Mid c,p,a ) by DIRAF:11;
then ( LIN c,a,p or LIN c,p,a ) by DIRAF:34;
hence contradiction by A15, DIRAF:36; :: thesis: verum

end;

A42: e5 <> e3

proof

assume e5 = e3 ; :: thesis: contradiction
then c,e3 // a,b by A39, DIRAF:5;
then p,c // a,b by A11, A20, DIRAF:6;
then c,p // b,a by DIRAF:5;
then b,c // b,a by A6, A8, DIRAF:6;
then ( Mid b,c,a or Mid b,a,c ) by DIRAF:11;
then ( LIN b,c,a or LIN b,a,c ) by DIRAF:34;
hence contradiction by A16, DIRAF:36; :: thesis: verum

end;

A43: e3,p // e3,c

proof

Mid p,c,e3 by A11, DIRAF:def 3;
then Mid e3,c,p by DIRAF:13;
then e3,c // c,p by DIRAF:def 3;
then e3,c // e3,p by ANALOAF:def 5;
hence e3,p // e3,c by DIRAF:5; :: thesis: verum

end;

A44: p,e2 // c,e5 by A13, A32, A37, DIRAF:6;
A45: LIN e2,e3,e5

proof

c,e1 // e4,c by A12, DIRAF:5;
then c,e1 // e2,e5 by A13, A33, DIRAF:6;
then p,a // e2,e5 by A9, A27, DIRAF:6;
then e2,e3 // e2,e5 by A3, A11, ANALOAF:def 5;
then ( Mid e2,e3,e5 or Mid e2,e5,e3 ) by DIRAF:11;
then ( LIN e2,e3,e5 or LIN e2,e5,e3 ) by DIRAF:34;
hence LIN e2,e3,e5 by DIRAF:36; :: thesis: verum

end;

A46: not LIN e3,e2,p by A23, DIRAF:36;
then not Mid e2,e3,e5 by A42, A43, A44, A45, Th24;
then ( Mid e3,e2,e5 or Mid e2,e5,e3 ) by A45, DIRAF:35;
then ( e3,e2 // e2,e5 or Mid e3,e5,e2 ) by DIRAF:13, DIRAF:def 3;
then ( e3,e2 // e3,e5 or e3,e5 // e5,e2 ) by ANALOAF:def 5, DIRAF:def 3;
then ( e3,e5 // e3,e2 & c,e5 // p,e2 & Mid p,c,e3 ) by A11, A44, ANALOAF:def 5, DIRAF:5, DIRAF:def 3;
then ( e3,e5 // e3,e2 & c,e5 // p,e2 & Mid e3,c,p ) by DIRAF:13;
then Mid e3,e5,e2 by A20, A46, Th22;
then Mid e2,e5,e3 by DIRAF:13;
then e2,e5 // e5,e3 by DIRAF:def 3;
then ( e2,e5 // e5,e3 & e2,e5 // e2,e3 ) by ANALOAF:def 5;
then e2,e3 // e5,e3 by A13, ANALOAF:def 5;
then p,a // e5,e3 by A11, A41, DIRAF:6;
then p,a // p,x by A21, A42, DIRAF:6;
then ( p,x // p,a & c,x // b,a ) by A40, DIRAF:5;
hence ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) by A1, A2, A8, A40, Th22; :: thesis: verum

end;

A47: ( b = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:4, DIRAF:14;
A48: ( a = c implies ( a,b // a,c & Mid p,a,a ) ) by DIRAF:7, DIRAF:14;
( p = c implies ( a,b // c,c & Mid p,c,a ) ) by DIRAF:7, DIRAF:14;
hence ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) by A7, A47, A48; :: thesis: verum