let OAS be OAffinSpace; :: thesis: for p, d, a, c, b being Element of OAS st Mid p,d,a & c,d // b,a & p,c // p,b & not LIN p,a,b & p <> c holds
Mid p,c,b
let p, d, a, c, b be Element of OAS; :: thesis: ( Mid p,d,a & c,d // b,a & p,c // p,b & not LIN p,a,b & p <> c implies Mid p,c,b )
assume that
A1: Mid p,d,a and
A2: c,d // b,a and
A3: p,c // p,b and
A4: not LIN p,a,b and
A5: p <> c ; :: thesis: Mid p,c,b
( Mid p,c,b or Mid p,b,c ) by A3, DIRAF:11;
then A6: ( LIN p,c,b or LIN p,b,c ) by DIRAF:34;
then A7: LIN p,c,b by DIRAF:36;
A8: p <> d

proof

assume p = d ; :: thesis: contradiction
then ( c,p // b,a & c,p // b,p ) by A2, A3, DIRAF:5;
then b,p // b,a by A5, ANALOAF:def 5;
then ( Mid b,p,a or Mid b,a,p ) by DIRAF:11;
then ( LIN b,p,a or LIN b,a,p ) by DIRAF:34;
hence contradiction by A4, DIRAF:36; :: thesis: verum

end;

now

assume A9: Mid p,b,c ; :: thesis: Mid p,c,b
p,d // d,a by A1, DIRAF:def 3;
then p,d // p,a by ANALOAF:def 5;
then A10: ( p,a // p,d & b,a // c,d & p <> b ) by A2, A4, DIRAF:5, DIRAF:37;
not LIN p,d,c

proof

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

end;

then Mid p,a,d by A9, A10, Th22;
then ( Mid d,a,p & Mid a,d,p ) by A1, DIRAF:13;
then c,a // b,a by A2, DIRAF:18;
then a,c // a,b by DIRAF:5;
then ( Mid a,c,b or Mid a,b,c ) by DIRAF:11;
then ( LIN a,c,b or LIN a,b,c ) by DIRAF:34;
then ( LIN b,c,a & LIN b,c,p & LIN b,c,b ) by A6, DIRAF:36, DIRAF:37;
then b = c by A4, DIRAF:38;
hence Mid p,c,b by DIRAF:14; :: thesis: verum

end;

hence Mid p,c,b by A3, DIRAF:11; :: thesis: verum