let OAS be OAffinSpace; :: thesis: for a, b, c, p 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 a, b, c, p 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 :: thesis: ( p <> c implies ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) )

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

A5: now :: thesis: ( p,b // c,p implies ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) )

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:2;
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, Th1;
p,a // d,p by A6, DIRAF:2;
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 :: thesis: ( p,b // p,c implies ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) )

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, Th2;
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 :: thesis: ( p = c implies ex d being Element of OAS st
( p,a '||' p,d & a,b '||' c,d ) )

A10: a,b '||' p,p by DIRAF:20;
A11: p,a '||' p,p by DIRAF:20;
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