let OAS be OAffinSpace; :: thesis: for p, b, c, a, d being Element of OAS st not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a holds
Mid c,p,d
let p, b, c, a, d be Element of OAS; :: thesis: ( not LIN p,b,c & Mid b,p,a & LIN p,c,d & b,c '||' d,a implies Mid c,p,d )
assume that
A1: not LIN p,b,c and
A2: Mid b,p,a and
A3: LIN p,c,d and
A4: b,c '||' d,a ; :: thesis: Mid c,p,d
A5: LIN p,d,c by A3, DIRAF:36;
LIN b,p,a by A2, DIRAF:34;
then A6: LIN p,b,a by DIRAF:36;
p,c '||' p,d by A3, DIRAF:def 5;
then A7: ( p,c // p,d or p,c // d,p ) by DIRAF:def 4;
assume A8: not Mid c,p,d ; :: thesis: contradiction
then A9: d <> p by DIRAF:14;

A10: now

assume p,c // d,p ; :: thesis: contradiction
then c,p // p,d by DIRAF:5;
hence contradiction by A8, DIRAF:def 3; :: thesis: verum

end;

p <> c by A8, DIRAF:14;
then consider q being Element of OAS such that
A11: p,b // p,q and
A12: b,c '||' d,q and
d <> q by A9, A7, A10, Th8;
A13: LIN p,d,p by DIRAF:37;
p,b '||' p,q by A11, DIRAF:def 4;
then LIN p,b,q by DIRAF:def 5;
then a = q by A1, A3, A4, A12, A6, Th11;
then b,p // p,q by A2, DIRAF:def 3;
then p,q // b,p by DIRAF:5;
then ( p,b // b,p or p = q ) by A11, DIRAF:6;
then ( p = b or p = q ) by ANALOAF:def 5;
then p,d '||' c,b by A1, A12, DIRAF:27, DIRAF:37;
then LIN p,d,b by A9, A5, DIRAF:39;
hence contradiction by A1, A9, A5, A13, DIRAF:38; :: thesis: verum