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

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

Mid b,p,c by A1, DIRAF:def 3;
then b,p,c are_collinear by DIRAF:28;
then A6: p,c,b are_collinear by DIRAF:30;
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 A7: a,p // b,p by DIRAF:2;
then a,p // p,c by A1, A3, DIRAF:3;
then Mid a,p,c by DIRAF:def 3;
then a,p,c are_collinear by DIRAF:28;
then p,c,a are_collinear by DIRAF:30;
then A8: p,c '||' a,b by A6, DIRAF:34;
A9: p,c // b,p by A1, DIRAF:2;
A10: p,c,c are_collinear by DIRAF:31;
consider d being Element of OAS such that
A11: Mid p,c,d and
A12: c <> d by DIRAF:13;
A13: p <> d by A11, A12, DIRAF:8;
p,c // c,d by A11, DIRAF:def 3;
then p,c // p,d by ANALOAF:def 5;
then A14: b,p // p,d by A2, A9, ANALOAF:def 5;
p,c,d are_collinear by A11, DIRAF:28;
then p,c '||' c,d by A10, DIRAF:34;
then a,b '||' c,d by A2, A8, DIRAF:23;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A7, A12, A13, A14, DIRAF:3; :: thesis: verum

end;

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

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 A16: a,p // p,b by DIRAF:2;
then Mid a,p,b by DIRAF:def 3;
then a,p,b are_collinear by DIRAF:28;
then A17: p,b,a are_collinear by DIRAF:30;
Mid b,p,c by A1, DIRAF:def 3;
then b,p,c are_collinear by DIRAF:28;
then A18: p,b,c are_collinear by DIRAF:30;
A19: a,b,b are_collinear by DIRAF:31;
A20: b <> c by A1, A2, ANALOAF:def 5;
p,b,b are_collinear by DIRAF:31;
then a,b,c are_collinear by A3, A17, A18, DIRAF:32;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A3, A16, A20, A19, DIRAF:34; :: thesis: verum

end;

assume a,b,p are_collinear ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )
then p,a,b are_collinear by DIRAF:30;
then p,a '||' p,b by DIRAF:def 5;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A5, A15, DIRAF:def 4; :: thesis: verum

end;

now :: thesis: ( not a,b,p are_collinear implies 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
A21: a,p // p,d and
A22: a,b // c,d by A1, A3, ANALOAF:def 5;
assume A23: not a,b,p are_collinear ; :: thesis: ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d )

A24: now :: thesis: not d = p

assume d = p ; :: thesis: contradiction
then p,c // b,a by A22, DIRAF:2;
then b,p // b,a by A1, A2, DIRAF:3;
then b,p '||' b,a by DIRAF:def 4;
then b,p,a are_collinear by DIRAF:def 5;
hence contradiction by A23, DIRAF:30; :: thesis: verum

end;

A25: now :: thesis: not d = c

assume d = c ; :: thesis: contradiction
then p,d // b,p by A1, DIRAF:2;
then a,p // b,p by A21, A24, DIRAF:3;
then p,a // p,b by DIRAF:2;
then p,a '||' p,b by DIRAF:def 4;
then p,a,b are_collinear by DIRAF:def 5;
hence contradiction by A23, DIRAF:30; :: thesis: verum

end;

a,b '||' c,d by A22, DIRAF:def 4;
hence ex d being Element of OAS st
( a,p // p,d & a,b '||' c,d & c <> d & p <> d ) by A21, A24, A25; :: 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