let OAS be OAffinSpace; :: thesis: for p, a, b, c, d being Element of 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 ; :: 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 b' being Element of such that
A7: c,p // p,b' and
A8: c,d // a,b' 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 <> b'

proof

assume A11: a = b' ; :: 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 // b',p by A7, DIRAF:5;
then p,b // b',p by A2, A9, DIRAF:6;
then A12: b',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 <> b'

proof

assume p = b' ; :: 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 b'' being Element of such that
A14: a,p // p,b'' and
A15: a,b' // b,b'' by A12, ANALOAF:def 5;
a <> p by A1, DIRAF:37;
then A16: a <> b'' by A14, ANALOAF:def 5;
b,a // a,b' by A3, A13, A8, DIRAF:6;
then b,a // b,b'' by A15, A10, DIRAF:6;
then ( Mid b,a,b'' or Mid b,b'',a ) by DIRAF:11;
then ( LIN b,a,b'' or LIN b,b'',a ) by DIRAF:34;
then A17: LIN a,b'',b by DIRAF:36;
Mid a,p,b'' by A14, DIRAF:def 3;
then LIN a,p,b'' by DIRAF:34;
then A18: LIN a,b'',p by DIRAF:36;
LIN a,b'',a by DIRAF:37;
hence contradiction by A1, A18, A16, A17, DIRAF:38; :: thesis: verum