let OAS be OAffinSpace; :: thesis: for a, b, c, p 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 a, b, c, p 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 :: thesis: ( not p,a,b are_collinear implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

assume A6: not p,a,b are_collinear ; :: 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, Th18;
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 ( b,a,p are_collinear or b,p,a are_collinear ) by DIRAF:28;
hence contradiction by A6, DIRAF:30; :: thesis: verum

end;

not p,x,c are_collinear

proof

( Mid p,a,x or Mid p,x,a ) by A7, DIRAF:7;
then ( p,a,x are_collinear or p,x,a are_collinear ) by DIRAF:28;
then A12: p,x,a are_collinear by DIRAF:30;
A13: p,x,p are_collinear by DIRAF:31;
p,b,c are_collinear by A2, DIRAF:28;
then A14: p,c,b are_collinear by DIRAF:30;
A15: p,c,p are_collinear by DIRAF:31;
assume p,x,c are_collinear ; :: thesis: contradiction
then p,c,a are_collinear 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, Th15; :: thesis: verum

end;

A16: now :: thesis: ( p,a,b are_collinear & c <> b implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

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

A19: now :: thesis: ( Mid p,a,b implies ( Mid p,a,a & b,a // c,a ) )

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 :: thesis: ( Mid p,b,a implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

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 :: thesis: ( b,a // a,c implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

A24: now :: thesis: ( p,a // a,c implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

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 :: thesis: ( a = b implies ex x being Element of OAS st
( Mid p,a,x & b,a // c,x ) )

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

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

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