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

now

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

A10: now

assume A11: ( e1 <> e2 & e2 <> p ) ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
p,b // e2,p by A9, DIRAF:5;
then e2,p // p,c by A1, A2, ANALOAF:def 5;
then consider x being Element of OAS such that
A12: ( e1,p // p,x & e1,e2 // c,x ) by A11, ANALOAF:def 5;
A13: b,a // c,x by A9, A11, A12, DIRAF:6;
p,a // p,x by A7, A8, A12, ANALOAF:def 5;
hence ex x being Element of OAS st
( p,a // p,x & b,a // c,x ) by A13; :: thesis: verum

end;

A14: now

assume A15: ( e1 = e2 & e2 <> p ) ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
then p,e2 // a,p by A8, DIRAF:5;
then b,p // a,p by A9, A15, DIRAF:6;
then p,b // p,a by DIRAF:5;
then A16: ( p,b // p,a & p,a // p,c ) by A1, A2, ANALOAF:def 5;
A17: ( p,b // b,a & p,a // a,c implies ( p,a // p,c & b,a // c,c ) ) by ANALOAF:def 5;

A18: now

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

end;

A19: now

assume ( p,a // a,b & p,a // a,c ) ; :: thesis: ( p,a // p,a & b,a // c,a )
then a,b // a,c by A6, ANALOAF:def 5;
hence ( p,a // p,a & b,a // c,a ) by DIRAF:4, DIRAF:5; :: thesis: verum

end;

now

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

end;

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

end;

now

assume p = e2 ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
then b,a // p,a by A7, A8, A9, DIRAF:6;
then A20: a,b // a,p by DIRAF:5;

A21: now

assume a,b // b,p ; :: thesis: ex x being Element of OAS st
( p,a // p,x & b,a // c,x )
then ( a,b // b,p & a,b // a,p ) by ANALOAF:def 5;
then A22: ( b,p // a,p or a = b ) by ANALOAF:def 5;

now

assume b,p // a,p ; :: thesis: ( p,a // p,c & b,a // c,c )
then a,p // c,p by A2, A3, ANALOAF:def 5;
hence ( p,a // p,c & b,a // c,c ) by DIRAF:5, DIRAF:7; :: thesis: verum

end;

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

end;

now

assume a,p // p,b ; :: thesis: ( p,a // p,p & b,a // c,p )
then ( a,p // p,b & a,p // a,b ) by ANALOAF:def 5;
then a,b // p,b by A6, ANALOAF:def 5;
then b,a // b,p by DIRAF:5;
hence ( p,a // p,p & b,a // c,p ) by A2, A3, DIRAF:6, DIRAF:7; :: thesis: verum

end;

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

end;

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

end;

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