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 ) )
assume A1: Mid p,c,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
then A2: p,c // c,b by DIRAF:def 3;
A3: ( p = c implies ( Mid p,p,a & b,a // c,p ) ) by DIRAF:7, DIRAF:14;

A4: now

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

end;

A5: ( b = c implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:4, DIRAF:14;

now

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

proof

Mid b,c,p by A1, DIRAF:13;
then b,c // c,p by DIRAF:def 3;
then ( b,c // c,p & b,c // b,p ) by ANALOAF:def 5;
hence b,p // c,p by A6, ANALOAF:def 5; :: thesis: verum

end;

A8: now

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

end;

now

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

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: ( Mid p,c,a implies ( Mid p,c,a & b,a // c,c ) ) by DIRAF:7;

now

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 & Mid b,a,p ) by A14, DIRAF:13;
then ( c,a // a,p & b,a // a,p ) by DIRAF:def 3;
then A16: ( a,p // c,a & a,p // b,a ) by DIRAF:5;
A17: ( a = p implies ( Mid p,p,a & b,a // c,p ) ) by A7, DIRAF:14;
( b,a // c,a implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:14;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A16, A17, ANALOAF:def 5; :: thesis: verum

end;

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

end;

A18: 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 A6, A7, ANALOAF:def 5, DIRAF:14; :: thesis: verum

end;

now

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

end;

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

end;

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

end;

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