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
A6: p <> d

proof

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

( Mid p,c,b or Mid p,b,c ) by A3, DIRAF:11;
then A8: ( LIN p,c,b or LIN p,b,c ) by DIRAF:34;
then A9: LIN p,c,b by DIRAF:36;

now

A10: not LIN p,d,c

proof

assume LIN p,d,c ; :: thesis: contradiction
then A11: LIN p,c,d by DIRAF:36;
LIN p,c,p by DIRAF:37;
then A12: LIN p,d,b by A5, A9, A11, DIRAF:38;
A13: LIN p,d,p by DIRAF:37;
LIN p,d,a by A1, DIRAF:34;
hence contradiction by A4, A6, A12, A13, DIRAF:38; :: thesis: verum

end;

assume A14: 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 A15: p,a // p,d by DIRAF:5;
A16: p <> b by A4, DIRAF:37;
b,a // c,d by A2, DIRAF:5;
then Mid p,a,d by A14, A15, A16, A10, Th22;
then A17: Mid d,a,p by DIRAF:13;
Mid a,d,p by A1, DIRAF:13;
then c,a // b,a by A2, A17, 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 A18: LIN b,c,a by DIRAF:36;
A19: LIN b,c,b by DIRAF:37;
LIN b,c,p by A8, DIRAF:36;
then b = c by A4, A18, A19, DIRAF:38;
hence Mid p,c,b by DIRAF:14; :: thesis: verum

end;

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