let OAS be OAffinSpace; :: thesis: for p, b, c, a, d being Element of OAS st Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b holds
Mid p,a,d
let p, b, c, a, d be Element of OAS; :: thesis: ( Mid p,b,c & LIN p,a,d & a,b '||' c,d & not LIN p,a,b implies Mid p,a,d )
assume that
A1: Mid p,b,c and
A2: LIN p,a,d and
A3: a,b '||' c,d and
A4: not LIN p,a,b ; :: thesis: Mid p,a,d

A5: now

assume b = c ; :: thesis: Mid p,a,d
then ( LIN p,b,b & LIN p,a,a & a,b '||' b,a & a,b '||' b,d ) by A3, DIRAF:24, DIRAF:37;
then a = d by A2, A4, Th11;
hence Mid p,a,d by DIRAF:14; :: thesis: verum

end;

now

assume A6: b <> c ; :: thesis: Mid p,a,d
then A7: p <> c by A1, DIRAF:12;
A8: b <> a by A4, DIRAF:37;
A9: not LIN d,b,a

proof

assume LIN d,b,a ; :: thesis: contradiction
then ( LIN a,b,d & a,b '||' d,c ) by A3, DIRAF:27, DIRAF:36;
then LIN a,b,c by A8, DIRAF:39;
then A10: LIN b,c,a by DIRAF:36;
LIN p,b,c by A1, DIRAF:34;
then ( LIN b,c,p & LIN b,c,b ) by DIRAF:36, DIRAF:37;
hence contradiction by A4, A6, A10, DIRAF:38; :: thesis: verum

end;

then A11: d <> a by DIRAF:37;
LIN d,a,p by A2, DIRAF:36;
then d,a '||' d,p by DIRAF:def 5;
then a,d '||' d,p by DIRAF:27;
then consider q being Element of OAS such that
A12: b,d '||' d,q and
A13: b,a '||' p,q by A11, DIRAF:32;
A14: not LIN b,c,d

proof

assume A15: LIN b,c,d ; :: thesis: contradiction
then A16: ( LIN b,c,d & LIN b,c,b ) by DIRAF:37;
LIN c,d,b by A15, DIRAF:36;
then A17: c,d '||' c,b by DIRAF:def 5;

now

assume a,b '||' c,b ; :: thesis: contradiction
then b,c '||' b,a by DIRAF:27;
then LIN b,c,a by DIRAF:def 5;
hence contradiction by A6, A9, A16, DIRAF:38; :: thesis: verum

end;

then ( LIN p,a,c & LIN p,b,c ) by A1, A2, A3, A17, DIRAF:28, DIRAF:34;
then ( LIN p,c,b & LIN p,c,c & LIN p,c,a ) by DIRAF:36, DIRAF:37;
then LIN b,c,a by A7, DIRAF:38;
hence contradiction by A6, A9, A16, DIRAF:38; :: thesis: verum

end;

A18: Mid d,b,q

proof

d,b '||' d,q by A12, DIRAF:27;
then LIN d,b,q by DIRAF:def 5;
then A19: LIN b,d,q by DIRAF:36;
a,b '||' q,p by A13, DIRAF:27;
then A20: c,d '||' q,p by A3, A8, DIRAF:28;
Mid c,b,p by A1, DIRAF:13;
hence Mid d,b,q by A14, A19, A20, Th13; :: thesis: verum

end;

assume A21: not Mid p,a,d ; :: thesis: contradiction
A22: d <> p

proof

assume d = p ; :: thesis: contradiction
then ( LIN p,b,c & p,c '||' b,a ) by A1, A3, DIRAF:27, DIRAF:34;
then ( LIN p,c,b & p,c '||' b,a ) by DIRAF:36;
then ( LIN p,c,p & LIN p,c,a & LIN p,c,b ) by A7, DIRAF:37, DIRAF:39;
hence contradiction by A4, A7, DIRAF:38; :: thesis: verum

end;

A23: not LIN d,p,q

proof

assume LIN d,p,q ; :: thesis: contradiction
then ( LIN d,p,p & LIN d,p,q & LIN d,p,a ) by A2, DIRAF:36, DIRAF:37;
then A24: LIN p,q,a by A22, DIRAF:38;
A25: p,q '||' a,b by A13, DIRAF:27;

now

assume p = q ; :: thesis: contradiction
then d,b '||' d,p by A12, DIRAF:27;
then LIN d,b,p by DIRAF:def 5;
then ( LIN d,p,d & LIN d,p,b & LIN d,p,a ) by A2, DIRAF:36, DIRAF:37;
hence contradiction by A9, A22, DIRAF:38; :: thesis: verum

end;

then ( p <> q & LIN p,q,p & LIN p,q,a & LIN p,q,b ) by A24, A25, DIRAF:37, DIRAF:39;
hence contradiction by A4, DIRAF:38; :: thesis: verum

end;

now

assume Mid p,d,a ; :: thesis: contradiction
then ( Mid p,d,a & d,b '||' d,q ) by A12, DIRAF:27;
then ( Mid p,d,a & LIN d,b,q ) by DIRAF:def 5;
then ( Mid p,d,a & LIN d,q,b & p,q '||' b,a ) by A13, DIRAF:27, DIRAF:36;
then Mid q,d,b by A23, Th13;
then Mid b,d,q by DIRAF:13;
then b = d by A18, DIRAF:18;
hence contradiction by A9, DIRAF:37; :: thesis: verum

end;

then ( Mid a,p,d & LIN p,b,c ) by A1, A2, A21, DIRAF:34, DIRAF:35;
then Mid b,p,c by A3, A4, Th13;
then p = b by A1, DIRAF:18;
hence contradiction by A4, DIRAF:37; :: thesis: verum

end;

hence Mid p,a,d by A5; :: thesis: verum