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
assume A5: not Mid c,p,d ; :: thesis: contradiction
then A6: ( d <> p & p <> c ) by DIRAF:14;
p,c '||' p,d by A3, DIRAF:def 5;
then A7: ( p,c // p,d or p,c // d,p ) by DIRAF:def 4;

now

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

end;

then consider q being Element of OAS such that
A8: p,b // p,q and
A9: b,c '||' d,q and
d <> q by A6, A7, Th8;
p,b '||' p,q by A8, DIRAF:def 4;
then A10: LIN p,b,q by DIRAF:def 5;
LIN b,p,a by A2, DIRAF:34;
then LIN p,b,a by DIRAF:36;
then a = q by A1, A3, A4, A9, A10, 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 A8, DIRAF:6;
then ( p = b or p = q ) by ANALOAF:def 5;
then ( LIN p,d,c & p,d '||' c,b ) by A1, A3, A9, DIRAF:27, DIRAF:36, DIRAF:37;
then ( LIN p,d,p & LIN p,d,c & LIN p,d,b ) by A6, DIRAF:37, DIRAF:39;
hence contradiction by A1, A6, DIRAF:38; :: thesis: verum