let OAS be OAffinSpace; :: thesis: for a, b, c, p being Element of OAS st p,b // p,c & p <> c & b <> p holds
ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d )
let a, b, c, p be Element of OAS; :: thesis: ( p,b // p,c & p <> c & b <> p implies ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d ) )
assume that
A1: p,b // p,c and
A2: p <> c and
A3: b <> p ; :: thesis: ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d )
consider q being Element of OAS such that
A4: Mid b,p,q and
A5: p <> q by DIRAF:13;
A6: b,p // p,q by A4, DIRAF:def 3;
then consider r being Element of OAS such that
A7: a,p // p,r and
A8: a,b '||' q,r and
A9: q <> r and
A10: r <> p by A3, A5, Th1;
b,p // c,p by A1, DIRAF:2;
then p,q // c,p by A3, A6, ANALOAF:def 5;
then q,p // p,c by DIRAF:2;
then consider d being Element of OAS such that
A11: r,p // p,d and
A12: r,q '||' c,d and
A13: c <> d and
d <> p by A2, A5, Th1;
p,r // d,p by A11, DIRAF:2;
then a,p // d,p by A7, A10, DIRAF:3;
then A14: p,a // p,d by DIRAF:2;
q,r '||' c,d by A12, DIRAF:22;
then a,b '||' c,d by A8, A9, DIRAF:23;
hence ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d ) by A13, A14; :: thesis: verum