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

LIN d,a,p by A2, DIRAF:30;
then d,a '||' d,p by DIRAF:def 5;
then A6: a,d '||' d,p by DIRAF:22;
assume A7: b <> c ; :: thesis: Mid p,a,d
A8: b <> a by A4, DIRAF:31;
A9: not LIN d,b,a

proof

assume LIN d,b,a ; :: thesis: contradiction
then A10: LIN a,b,d by DIRAF:30;
a,b '||' d,c by A3, DIRAF:22;
then LIN a,b,c by A8, A10, DIRAF:33;
then A11: LIN b,c,a by DIRAF:30;
LIN p,b,c by A1, DIRAF:28;
then A12: LIN b,c,p by DIRAF:30;
LIN b,c,b by DIRAF:31;
hence contradiction by A4, A7, A11, A12, DIRAF:32; :: thesis: verum

end;

then d <> a by DIRAF:31;
then consider q being Element of OAS such that
A13: b,d '||' d,q and
A14: b,a '||' p,q by A6, DIRAF:27;
A15: LIN p,b,c by A1, DIRAF:28;
A16: p <> c by A1, A7, DIRAF:8;
A17: not LIN b,c,d

proof

A18: LIN p,c,c by DIRAF:31;
LIN p,b,c by A1, DIRAF:28;
then A19: LIN p,c,b by DIRAF:30;
assume A20: LIN b,c,d ; :: thesis: contradiction
A21: LIN b,c,b by DIRAF:31;

A22: now

assume a,b '||' c,b ; :: thesis: contradiction
then b,c '||' b,a by DIRAF:22;
then LIN b,c,a by DIRAF:def 5;
hence contradiction by A7, A9, A20, A21, DIRAF:32; :: thesis: verum

end;

LIN c,d,b by A20, DIRAF:30;
then c,d '||' c,b by DIRAF:def 5;
then LIN p,a,c by A2, A3, A22, DIRAF:23;
then LIN p,c,a by DIRAF:30;
then LIN b,c,a by A16, A19, A18, DIRAF:32;
hence contradiction by A7, A9, A20, A21, DIRAF:32; :: thesis: verum

end;

a,b '||' q,p by A14, DIRAF:22;
then A23: c,d '||' q,p by A3, A8, DIRAF:23;
d,b '||' d,q by A13, DIRAF:22;
then LIN d,b,q by DIRAF:def 5;
then A24: LIN b,d,q by DIRAF:30;
A25: d <> p

proof

A26: LIN p,c,p by DIRAF:31;
LIN p,b,c by A1, DIRAF:28;
then A27: LIN p,c,b by DIRAF:30;
assume d = p ; :: thesis: contradiction
then p,c '||' b,a by A3, DIRAF:22;
then LIN p,c,a by A16, A27, DIRAF:33;
hence contradiction by A4, A16, A27, A26, DIRAF:32; :: thesis: verum

end;

A28: not LIN d,p,q

proof

A29: now

assume p = q ; :: thesis: contradiction
then d,b '||' d,p by A13, DIRAF:22;
then LIN d,b,p by DIRAF:def 5;
then A30: LIN d,p,b by DIRAF:30;
A31: LIN d,p,d by DIRAF:31;
LIN d,p,a by A2, DIRAF:30;
hence contradiction by A9, A25, A31, A30, DIRAF:32; :: thesis: verum

end;

A32: LIN p,q,p by DIRAF:31;
A33: LIN d,p,p by DIRAF:31;
assume A34: LIN d,p,q ; :: thesis: contradiction
LIN d,p,a by A2, DIRAF:30;
then A35: LIN p,q,a by A25, A34, A33, DIRAF:32;
p,q '||' a,b by A14, DIRAF:22;
then LIN p,q,b by A35, A29, DIRAF:33;
hence contradiction by A4, A35, A29, A32, DIRAF:32; :: thesis: verum

end;

Mid c,b,p by A1, DIRAF:9;
then A36: Mid d,b,q by A17, A24, A23, Th13;

A37: now

d,b '||' d,q by A13, DIRAF:22;
then LIN d,b,q by DIRAF:def 5;
then A38: LIN d,q,b by DIRAF:30;
assume A39: Mid p,d,a ; :: thesis: contradiction
p,q '||' b,a by A14, DIRAF:22;
then Mid q,d,b by A28, A39, A38, Th13;
then Mid b,d,q by DIRAF:9;
then b = d by A36, DIRAF:14;
hence contradiction by A9, DIRAF:31; :: thesis: verum

end;

assume not Mid p,a,d ; :: thesis: contradiction
then Mid a,p,d by A2, A37, DIRAF:29;
then Mid b,p,c by A3, A4, A15, Th13;
then p = b by A1, DIRAF:14;
hence contradiction by A4, DIRAF:31; :: thesis: verum

end;

now

A40: a,b '||' b,a by DIRAF:19;
A41: LIN p,a,a by DIRAF:31;
A42: LIN p,b,b by DIRAF:31;
assume b = c ; :: thesis: Mid p,a,d
then a = d by A2, A3, A4, A42, A41, A40, Th11;
hence Mid p,a,d by DIRAF:10; :: thesis: verum

end;

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