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

A5: now

Mid b,p,c by A1, DIRAF:def 3;
then LIN b,p,c by DIRAF:34;
then A6: LIN p,c,b by DIRAF:36;
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:5;
then a,p // p,c by A1, A3, DIRAF:6;
then Mid a,p,c by DIRAF:def 3;
then LIN a,p,c by DIRAF:34;
then LIN p,c,a by DIRAF:36;
then A8: p,c '||' a,b by A6, DIRAF:40;
A9: p,c // b,p by A1, DIRAF:5;
A10: LIN p,c,c by DIRAF:37;
consider d being Element of OAS such that
A11: Mid p,c,d and
A12: c <> d by DIRAF:17;
A13: p <> d by A11, A12, DIRAF:12;
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;
LIN p,c,d by A11, DIRAF:34;
then p,c '||' c,d by A10, DIRAF:40;
then a,b '||' c,d by A2, A8, DIRAF:28;
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:6; :: thesis: verum

end;

A15: 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 A16: a,p // p,b by DIRAF:5;
then Mid a,p,b by DIRAF:def 3;
then LIN a,p,b by DIRAF:34;
then A17: LIN p,b,a by DIRAF:36;
Mid b,p,c by A1, DIRAF:def 3;
then LIN b,p,c by DIRAF:34;
then A18: LIN p,b,c by DIRAF:36;
A19: LIN a,b,b by DIRAF:37;
A20: b <> c by A1, A2, ANALOAF:def 5;
LIN p,b,b by DIRAF:37;
then LIN a,b,c by A3, A17, A18, DIRAF:38;
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:40; :: thesis: verum

end;

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 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

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

A24: now

assume d = p ; :: thesis: contradiction
then p,c // b,a by A22, 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 A23, DIRAF:36; :: thesis: verum

end;

A25: now

assume d = c ; :: thesis: contradiction
then p,d // b,p by A1, DIRAF:5;
then a,p // b,p by A21, A24, 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 A23, DIRAF:36; :: 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