let OAS be OAffinSpace; :: thesis: for p, b, c, a 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 p, b, c, a 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:17;
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, Th7;
b,p // c,p by A1, DIRAF:5;
then p,q // c,p by A3, A6, ANALOAF:def 5;
then q,p // p,c by DIRAF:5;
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, Th7;
q,r '||' c,d by A12, DIRAF:27;
then A14: a,b '||' c,d by A8, A9, DIRAF:28;
p,r // d,p by A11, DIRAF:5;
then a,p // d,p by A7, A10, DIRAF:6;
then p,a // p,d by DIRAF:5;
hence ex d being Element of OAS st
( p,a // p,d & a,b '||' c,d & c <> d ) by A13, A14; :: thesis: verum