let OAS be OAffinSpace; :: thesis: for p, a, b, c, d being Element of OAS st not LIN p,a,b & p,b // p,c & b,a // c,d & p <> d holds
not Mid a,p,d
let p, a, b, c, d be Element of OAS; :: thesis: ( not LIN p,a,b & p,b // p,c & b,a // c,d & p <> d implies not Mid a,p,d )
assume that
A1: not LIN p,a,b and
A2: p,b // p,c and
A3: b,a // c,d and
A4: p <> d ; :: thesis: not Mid a,p,d
assume Mid a,p,d ; :: thesis: contradiction
then Mid d,p,a by DIRAF:13;
then A5: d,p // p,a by DIRAF:def 3;
then A6: p,d // a,p by DIRAF:5;
consider b9 being Element of OAS such that
A7: c,p // p,b9 and
A8: c,d // a,b9 by A4, A5, ANALOAF:def 5;
A9: p <> c

proof

assume p = c ; :: thesis: contradiction
then b,a // a,p by A3, A4, A6, DIRAF:6;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1, DIRAF:13, DIRAF:34; :: thesis: verum

end;

A10: a <> b9

proof

assume A11: a = b9 ; :: thesis: contradiction
b,p // c,p by A2, DIRAF:5;
then b,p // p,a by A9, A7, A11, DIRAF:6;
then Mid b,p,a by DIRAF:def 3;
then LIN b,p,a by DIRAF:34;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

p,c // b9,p by A7, DIRAF:5;
then p,b // b9,p by A2, A9, DIRAF:6;
then A12: b9,p // p,b by DIRAF:5;
A13: c <> d

proof

assume c = d ; :: thesis: contradiction
then p,b // a,p by A2, A4, A6, DIRAF:6;
then b,p // p,a by DIRAF:5;
then Mid b,p,a by DIRAF:def 3;
then LIN b,p,a by DIRAF:34;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

p <> b9

proof

assume p = b9 ; :: thesis: contradiction
then b,a // a,p by A3, A13, A8, DIRAF:6;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1, DIRAF:13, DIRAF:34; :: thesis: verum

end;

then consider b99 being Element of OAS such that
A14: a,p // p,b99 and
A15: a,b9 // b,b99 by A12, ANALOAF:def 5;
a <> p by A1, DIRAF:37;
then A16: a <> b99 by A14, ANALOAF:def 5;
b,a // a,b9 by A3, A13, A8, DIRAF:6;
then b,a // b,b99 by A15, A10, DIRAF:6;
then ( Mid b,a,b99 or Mid b,b99,a ) by DIRAF:11;
then ( LIN b,a,b99 or LIN b,b99,a ) by DIRAF:34;
then A17: LIN a,b99,b by DIRAF:36;
Mid a,p,b99 by A14, DIRAF:def 3;
then LIN a,p,b99 by DIRAF:34;
then A18: LIN a,b99,p by DIRAF:36;
LIN a,b99,a by DIRAF:37;
hence contradiction by A1, A18, A16, A17, DIRAF:38; :: thesis: verum