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 & LIN a,p,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 & LIN a,p,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
LIN a,p,d and
A4: p <> d ; :: thesis: not Mid a,p,d
A5: a <> p by A1, DIRAF:37;
assume Mid a,p,d ; :: thesis: contradiction
then Mid d,p,a by DIRAF:13;
then A6: d,p // p,a by DIRAF:def 3;
then A7: p,d // a,p by DIRAF:5;
A8: p <> c

proof

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

end;

A9: c <> d

proof

assume c = d ; :: thesis: contradiction
then p,b // a,p by A2, A4, A7, 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;

consider b' being Element of OAS such that
A10: ( c,p // p,b' & c,d // a,b' ) by A4, A6, ANALOAF:def 5;
A11: p <> b'

proof

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

end;

p,c // b',p by A10, DIRAF:5;
then p,b // b',p by A2, A8, DIRAF:6;
then b',p // p,b by DIRAF:5;
then consider b'' being Element of OAS such that
A12: ( a,p // p,b'' & a,b' // b,b'' ) by A11, ANALOAF:def 5;
Mid a,p,b'' by A12, DIRAF:def 3;
then LIN a,p,b'' by DIRAF:34;
then A13: LIN a,b'',p by DIRAF:36;
A14: a <> b'' by A5, A12, ANALOAF:def 5;
A15: a <> b'

proof

assume a = b' ; :: thesis: contradiction
then ( c,p // p,a & b,p // c,p ) by A2, A10, DIRAF:5;
then b,p // p,a by A8, 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;

b,a // a,b' by A3, A9, A10, DIRAF:6;
then b,a // b,b'' by A12, A15, 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 ( LIN a,b'',b & LIN a,b'',a ) by DIRAF:36, DIRAF:37;
hence contradiction by A1, A13, A14, DIRAF:38; :: thesis: verum