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

A4: now

assume A5: not LIN a,b,p ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )
consider d being Element of OAS such that
A6: a,p // p,d and
A7: a,b // c,d by A1, A3, ANALOAF:def 5;

A8: now

assume d = p ; :: thesis: contradiction
then p,c // b,a by A7, DIRAF:5;
then b,p // b,a by A1, A2, DIRAF:6;
then b,p '||' b,a by DIRAF:def 4;
then LIN b,p,a by DIRAF:def 5;
hence contradiction by A5, DIRAF:36; :: thesis: verum

end;

A9: now

assume d = c ; :: thesis: contradiction
then p,d // b,p by A1, DIRAF:5;
then a,p // b,p by A6, A8, DIRAF:6;
then p,a // p,b by DIRAF:5;
then p,a '||' p,b by DIRAF:def 4;
then LIN p,a,b by DIRAF:def 5;
hence contradiction by A5, DIRAF:36; :: thesis: verum

end;

a,b '||' c,d by A7, DIRAF:def 4;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A6, A8, A9; :: thesis: verum

end;

now

assume LIN a,b,p ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )
then LIN p,a,b by DIRAF:36;
then A10: p,a '||' p,b by DIRAF:def 5;

A11: now

assume p,a // p,b ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )
then A12: a,p // b,p by DIRAF:5;
Mid b,p,c by A1, DIRAF:def 3;
then A13: LIN b,p,c by DIRAF:34;
consider d being Element of OAS such that
A14: Mid p,c,d and
A15: c <> d by DIRAF:17;
A16: p <> d by A14, A15, DIRAF:12;
p,c // c,d by A14, DIRAF:def 3;
then ( p,c // b,p & p,c // p,d ) by A1, ANALOAF:def 5, DIRAF:5;
then A17: b,p // p,d by A2, ANALOAF:def 5;
a,p // p,c by A1, A3, A12, DIRAF:6;
then Mid a,p,c by DIRAF:def 3;
then LIN a,p,c by DIRAF:34;
then ( LIN p,c,a & LIN p,c,b ) by A13, DIRAF:36;
then A18: p,c '||' a,b by DIRAF:40;
( LIN p,c,c & LIN p,c,d ) by A14, DIRAF:34, DIRAF:37;
then p,c '||' c,d by DIRAF:40;
then a,b '||' c,d by A2, A18, DIRAF:28;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A12, A15, A16, A17, DIRAF:6; :: thesis: verum

end;

now

assume p,a // b,p ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )
then A19: a,p // p,b by DIRAF:5;
A20: b <> c by A1, A2, ANALOAF:def 5;
( Mid a,p,b & Mid b,p,c ) by A1, A19, DIRAF:def 3;
then ( LIN a,p,b & LIN b,p,c ) by DIRAF:34;
then ( LIN p,b,a & LIN p,b,b & LIN p,b,c ) by DIRAF:36, DIRAF:37;
then ( LIN a,b,c & LIN a,b,b ) by A3, DIRAF:38;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A19, A20, DIRAF:40; :: thesis: verum

end;

hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A10, A11, DIRAF:def 4; :: thesis: verum

end;

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