let OAS be OAffinSpace; :: thesis: for p, b, c, a being Element of OAS st p <> b & Mid p,b,c holds
ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
let p, b, c, a be Element of OAS; :: thesis: ( p <> b & Mid p,b,c implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )
assume that
A1: p <> b and
A2: Mid p,b,c ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
A3: p,b // b,c by A2, DIRAF:def 3;
then A4: p,b // p,c by ANALOAF:def 5;

A5: now

assume A6: not LIN p,a,b ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
consider x being Element of OAS such that
A7: p,a // p,x and
A8: b,a // c,x by A1, A4, Th25;
A9: p <> c by A1, A2, DIRAF:8;
A10: p <> x

proof

p,b // p,c by A2, DIRAF:7;
then A11: c,p // b,p by DIRAF:2;
assume p = x ; :: thesis: contradiction
then b,a // b,p by A8, A9, A11, DIRAF:3;
then ( Mid b,a,p or Mid b,p,a ) by DIRAF:7;
then ( LIN b,a,p or LIN b,p,a ) by DIRAF:28;
hence contradiction by A6, DIRAF:30; :: thesis: verum

end;

not LIN p,x,c

proof

( Mid p,a,x or Mid p,x,a ) by A7, DIRAF:7;
then ( LIN p,a,x or LIN p,x,a ) by DIRAF:28;
then A12: LIN p,x,a by DIRAF:30;
A13: LIN p,x,p by DIRAF:31;
LIN p,b,c by A2, DIRAF:28;
then A14: LIN p,c,b by DIRAF:30;
A15: LIN p,c,p by DIRAF:31;
assume LIN p,x,c ; :: thesis: contradiction
then LIN p,c,a by A10, A12, A13, DIRAF:32;
hence contradiction by A6, A9, A14, A15, DIRAF:32; :: thesis: verum

end;

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

end;

A16: now

assume that
A17: LIN p,a,b and
A18: c <> b ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )

A19: now

assume Mid p,a,b ; :: thesis: ( Mid p,a,a & b,a // c,a )
then Mid a,b,c by A2, DIRAF:11;
then Mid c,b,a by DIRAF:9;
then A20: c,b // b,a by DIRAF:def 3;
then c,b // c,a by ANALOAF:def 5;
hence ( Mid p,a,a & b,a // c,a ) by A18, A20, ANALOAF:def 5, DIRAF:10; :: thesis: verum

end;

A21: now

assume Mid p,b,a ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
then A22: p,b // b,a by DIRAF:def 3;

A23: now

A24: now

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

end;

A25: now

assume a = b ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
then b,a // c,a by DIRAF:4;
hence ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) by DIRAF:10; :: thesis: verum

end;

p,b // p,a by A22, ANALOAF:def 5;
then A26: b,a // p,a by A1, A22, ANALOAF:def 5;
assume b,a // a,c ; :: thesis: ex x being Element of OAS st
( Mid p,a,x & b,a // c,x )
hence ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) by A26, A25, A24, ANALOAF:def 5; :: thesis: verum

end;

A27: now

assume A28: b,c // c,a ; :: thesis: ( Mid p,a,a & b,a // c,a )
then b,c // b,a by ANALOAF:def 5;
hence ( Mid p,a,a & b,a // c,a ) by A18, A28, ANALOAF:def 5, DIRAF:10; :: thesis: verum

end;

b,a // b,c by A1, A3, A22, ANALOAF:def 5;
hence ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) by A23, A27, ANALOAF:def 5; :: thesis: verum

end;

now

assume Mid a,p,b ; :: thesis: ( Mid p,a,a & b,a // c,a )
then Mid a,b,c by A1, A2, DIRAF:12;
then Mid c,b,a by DIRAF:9;
then A29: c,b // b,a by DIRAF:def 3;
then c,b // c,a by ANALOAF:def 5;
hence ( Mid p,a,a & b,a // c,a ) by A18, A29, ANALOAF:def 5, DIRAF:10; :: thesis: verum

end;

hence ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) by A17, A19, A21, DIRAF:29; :: thesis: verum

end;

( c = b implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:1, DIRAF:10;
hence ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) by A5, A16; :: thesis: verum