let OAS be OAffinSpace; :: thesis: for p, c, b, a being Element of OAS st Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
let p, c, b, a be Element of OAS; :: thesis: ( Mid p,c,b implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
A1: ( b = c implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:4, DIRAF:14;
assume A2: Mid p,c,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )

A3: now

assume p = b ; :: thesis: ( Mid p,p,a & b,a // c,p )
then p = c by A2, DIRAF:12;
hence ( Mid p,p,a & b,a // c,p ) by DIRAF:7, DIRAF:14; :: thesis: verum

end;

A4: p,c // c,b by A2, DIRAF:def 3;

A5: now

assume that
A6: p <> c and
A7: p <> b and
A8: b <> c ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
Mid b,c,p by A2, DIRAF:13;
then A9: b,c // c,p by DIRAF:def 3;
then A10: b,c // b,p by ANALOAF:def 5;
then A11: b,p // c,p by A8, A9, ANALOAF:def 5;

A12: now

A13: now

assume A14: Mid p,a,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )

A15: now

Mid b,a,p by A14, DIRAF:13;
then b,a // a,p by DIRAF:def 3;
then A16: a,p // b,a by DIRAF:5;
assume Mid p,a,c ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
then Mid c,a,p by DIRAF:13;
then c,a // a,p by DIRAF:def 3;
then A17: a,p // c,a by DIRAF:5;
A18: ( b,a // c,a implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:14;
( a = p implies ( Mid p,p,a & b,a // c,p ) ) by A8, A9, A10, ANALOAF:def 5, DIRAF:14;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A17, A16, A18, ANALOAF:def 5; :: thesis: verum

end;

( Mid p,c,a implies ( Mid p,c,a & b,a // c,c ) ) by DIRAF:7;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A2, A14, A15, DIRAF:21; :: thesis: verum

end;

A19: now

assume Mid a,p,b ; :: thesis: ( Mid p,p,a & b,a // c,p )
then Mid b,p,a by DIRAF:13;
then b,p // p,a by DIRAF:def 3;
then b,p // b,a by ANALOAF:def 5;
hence ( Mid p,p,a & b,a // c,p ) by A7, A11, ANALOAF:def 5, DIRAF:14; :: thesis: verum

end;

A20: now

A21: p,c // p,b by A4, ANALOAF:def 5;
assume A22: Mid p,b,a ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
then p,b // b,a by DIRAF:def 3;
then p,c // b,a by A7, A21, DIRAF:6;
then b,a // c,b by A4, A6, ANALOAF:def 5;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A22; :: thesis: verum

end;

assume LIN p,a,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A13, A19, A20, DIRAF:35; :: thesis: verum

end;

now

A23: p,b // p,c by A2, DIRAF:11;
assume A24: not LIN p,a,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
then p <> b by DIRAF:37;
then consider x being Element of OAS such that
A25: p,a // p,x and
A26: b,a // c,x by A23, Th25;
A27: p,x // p,a by A25, DIRAF:5;
c,x // b,a by A26, DIRAF:5;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A2, A6, A24, A26, A27, Th22; :: thesis: verum

end;

hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A12; :: thesis: verum

end;

( p = c implies ( Mid p,p,a & b,a // c,p ) ) by DIRAF:7, DIRAF:14;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A3, A1, A5; :: thesis: verum