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:2;
then b,p // b,a by A2, A5, A7, ANALOAF:def 5;
then ( Mid b,p,a or Mid b,a,p ) by DIRAF:7;
then ( LIN b,p,a or LIN b,a,p ) by DIRAF:28;
hence contradiction by A4, DIRAF:30; :: thesis: verum

end;

( Mid p,c,b or Mid p,b,c ) by A3, DIRAF:7;
then A8: ( LIN p,c,b or LIN p,b,c ) by DIRAF:28;
then A9: LIN p,c,b by DIRAF:30;

now

A10: not LIN p,d,c

proof

assume LIN p,d,c ; :: thesis: contradiction
then A11: LIN p,c,d by DIRAF:30;
LIN p,c,p by DIRAF:31;
then A12: LIN p,d,b by A5, A9, A11, DIRAF:32;
A13: LIN p,d,p by DIRAF:31;
LIN p,d,a by A1, DIRAF:28;
hence contradiction by A4, A6, A12, A13, DIRAF:32; :: 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:2;
A16: p <> b by A4, DIRAF:31;
b,a // c,d by A2, DIRAF:2;
then Mid p,a,d by A14, A15, A16, A10, Th22;
then A17: Mid d,a,p by DIRAF:9;
Mid a,d,p by A1, DIRAF:9;
then c,a // b,a by A2, A17, DIRAF:14;
then a,c // a,b by DIRAF:2;
then ( Mid a,c,b or Mid a,b,c ) by DIRAF:7;
then ( LIN a,c,b or LIN a,b,c ) by DIRAF:28;
then A18: LIN b,c,a by DIRAF:30;
A19: LIN b,c,b by DIRAF:31;
LIN b,c,p by A8, DIRAF:30;
then b = c by A4, A18, A19, DIRAF:32;
hence Mid p,c,b by DIRAF:10; :: thesis: verum

end;

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