let OAS be OAffinSpace; :: thesis: for a, b, c, p 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 a, b, c, p 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:1, DIRAF:10;
assume A2: Mid p,c,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
A3: now :: thesis: ( p = b implies ( Mid p,p,a & b,a // c,p ) )
assume p = b ; :: thesis: ( Mid p,p,a & b,a // c,p )
then p = c by A2, DIRAF:8;
hence ( Mid p,p,a & b,a // c,p ) by DIRAF:4, DIRAF:10; :: thesis: verum
end;
A4: p,c // c,b by A2, DIRAF:def 3;
A5: now :: thesis: ( p <> c & p <> b & b <> c implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
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:9;
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 :: thesis: ( p,a,b are_collinear implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
A13: now :: thesis: ( Mid p,a,b implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
assume A14: Mid p,a,b ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
A15: now :: thesis: ( Mid p,a,c implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
Mid b,a,p by A14, DIRAF:9;
then b,a // a,p by DIRAF:def 3;
then A16: a,p // b,a by DIRAF:2;
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:9;
then c,a // a,p by DIRAF:def 3;
then A17: a,p // c,a by DIRAF:2;
A18: ( b,a // c,a implies ( Mid p,a,a & b,a // c,a ) ) by DIRAF:10;
( a = p implies ( Mid p,p,a & b,a // c,p ) ) by A8, A9, A10, ANALOAF:def 5, DIRAF:10;
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:4;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A2, A14, A15, DIRAF:17; :: thesis: verum
end;
A19: now :: thesis: ( Mid a,p,b implies ( Mid p,p,a & b,a // c,p ) )
assume Mid a,p,b ; :: thesis: ( Mid p,p,a & b,a // c,p )
then Mid b,p,a by DIRAF:9;
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:10; :: thesis: verum
end;
A20: now :: thesis: ( Mid p,b,a implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
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:3;
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 p,a,b are_collinear ; :: 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:29; :: thesis: verum
end;
now :: thesis: ( not p,a,b are_collinear implies ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) )
A23: p,b // p,c by A2, DIRAF:7;
assume A24: not p,a,b are_collinear ; :: thesis: ex x being Element of OAS st
( Mid p,x,a & b,a // c,x )
then p <> b by DIRAF:31;
then consider x being Element of OAS such that
A25: p,a // p,x and
A26: b,a // c,x by A23, Th18;
A27: p,x // p,a by A25, DIRAF:2;
c,x // b,a by A26, DIRAF:2;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A2, A6, A24, A26, A27, Th15; :: 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:4, DIRAF:10;
hence ex x being Element of OAS st
( Mid p,x,a & b,a // c,x ) by A3, A1, A5; :: thesis: verum