let OAS be OAffinSpace; :: thesis: for p, b, c, a being Element of OAS st p,b '||' p,c & p <> b holds
ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )
let p, b, c, a be Element of OAS; :: thesis: ( p,b '||' p,c & p <> b implies ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) )
assume that
A1: p,b '||' p,c and
A2: p <> b ; :: thesis: ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )

A3: now

assume A4: p <> c ; :: thesis: ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )

A5: now

assume p,b // c,p ; :: thesis: ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )
then b,p // p,c by DIRAF:5;
then consider d being Element of OAS such that
A6: a,p // p,d and
A7: a,b '||' c,d and
c <> d and
d <> p by A2, A4, Th7;
p,a // d,p by A6, DIRAF:5;
then p,a '||' p,d by DIRAF:def 4;
hence ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) by A7; :: thesis: verum

end;

now

assume p,b // p,c ; :: thesis: ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )
then consider d being Element of OAS such that
A8: p,a // p,d and
A9: a,b '||' c,d and
c <> d by A2, A4, Th8;
p,a '||' p,d by A8, DIRAF:def 4;
hence ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) by A9; :: thesis: verum

end;

hence ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) by A1, A5, DIRAF:def 4; :: thesis: verum

end;

now

A10: a,b '||' p,p by DIRAF:25;
A11: p,a '||' p,p by DIRAF:25;
assume p = c ; :: thesis: ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d )
hence ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) by A11, A10; :: thesis: verum

end;

hence ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) by A3; :: thesis: verum