let OAS be OAffinSpace; :: thesis: for p, c, b, d, a being Element of OAS st Mid p,c,b & c,d // b,a & p,d // p,a & not LIN p,a,b & p <> c holds
Mid p,d,a
let p, c, b, d, a be Element of OAS; :: thesis: ( Mid p,c,b & c,d // b,a & p,d // p,a & not LIN p,a,b & p <> c implies Mid p,d,a )
assume that
A1: Mid p,c,b and
A2: c,d // b,a and
A3: p,d // p,a and
A4: not LIN p,a,b and
A5: p <> c ; :: thesis: Mid p,d,a
A6: LIN p,c,b by A1, DIRAF:34;

now

assume A7: Mid p,a,d ; :: thesis: Mid p,d,a
then A8: LIN p,a,d by DIRAF:34;

A9: now

assume A10: ( b <> c & d <> a ) ; :: thesis: Mid p,d,a
A11: ( p <> a & p <> b & a <> b ) by A4, DIRAF:37;
assume not Mid p,d,a ; :: thesis: contradiction
then Mid p,a,d by A3, DIRAF:11;
then p,a // a,d by DIRAF:def 3;
then consider e1 being Element of OAS such that
A12: c,a // a,e1 and
A13: c,p // d,e1 by A11, ANALOAF:def 5;
A14: Mid c,a,e1 by A12, DIRAF:def 3;
then A15: LIN c,a,e1 by DIRAF:34;
consider e2 being Element of OAS such that
A16: b,a // a,e2 and
A17: b,c // e1,e2 by A4, A6, A12, ANALOAF:def 5;
Mid b,a,e2 by A16, DIRAF:def 3;
then LIN b,a,e2 by DIRAF:34;
then A18: LIN a,e2,b by DIRAF:36;
A19: b <> e2 by A11, A16, ANALOAF:def 5;
A20: d <> e1

proof

assume d = e1 ; :: thesis: contradiction
then LIN c,a,d by A14, DIRAF:34;
then ( LIN a,d,c & ( Mid p,d,a or Mid p,a,d ) ) by A3, DIRAF:11, DIRAF:36;
then ( LIN a,d,c & ( LIN p,d,a or LIN p,a,d ) ) by DIRAF:34;
then ( LIN d,a,c & LIN d,a,p ) by DIRAF:36;
then ( LIN d,a,b & LIN d,a,p & LIN d,a,a ) by A5, A6, DIRAF:37, DIRAF:41;
hence contradiction by A4, A10, DIRAF:38; :: thesis: verum

end;

A21: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then Mid c,a,c by A12, DIRAF:def 3;
hence contradiction by A4, A6, DIRAF:12; :: thesis: verum

end;

consider e3 being Element of OAS such that
A22: b,c // e2,e3 and
A23: ( b,e2 // c,e3 & c <> e3 ) by ANALOAF:def 5;
A24: LIN d,e3,c

proof

b,a // b,e2 by A16, ANALOAF:def 5;
then c,d // b,e2 by A2, A11, DIRAF:6;
then c,d // c,e3 by A19, A23, DIRAF:6;
then ( Mid c,d,e3 or Mid c,e3,d ) by DIRAF:11;
then ( LIN c,d,e3 or LIN c,e3,d ) by DIRAF:34;
hence LIN d,e3,c by DIRAF:36; :: thesis: verum

end;

Mid b,c,p by A1, DIRAF:13;
then A25: b,c // c,p by DIRAF:def 3;
then e1,e2 // c,p by A10, A17, ANALOAF:def 5;
then A26: e1,e2 // d,e1 by A5, A13, DIRAF:6;
then d,e1 // e1,e2 by DIRAF:5;
then A27: d,e1 // d,e2 by ANALOAF:def 5;
then ( d,e2 // d,e1 & d,e1 // c,p ) by A13, DIRAF:5;
then ( d,e2 // c,p & c,p // b,c ) by A20, A25, DIRAF:5, DIRAF:6;
then d,e2 // b,c by A5, DIRAF:6;
then A28: d,e2 // e2,e3 by A10, A22, DIRAF:6;
then Mid d,e2,e3 by DIRAF:def 3;
then A29: LIN d,e2,e3 by DIRAF:34;
A30: d <> e2 by A20, A26, ANALOAF:def 5;
then A31: d <> e3 by A28, ANALOAF:def 5;
A32: a <> e1

proof

assume A33: a = e1 ; :: thesis: contradiction
p,a // a,d by A7, DIRAF:def 3;
then d,a // a,p by DIRAF:5;
then c,p // a,p by A10, A13, A33, DIRAF:6;
then p,c // p,a by DIRAF:5;
then ( Mid p,c,a or Mid p,a,c ) by DIRAF:11;
then ( LIN p,c,a or LIN p,a,c ) by DIRAF:34;
then ( LIN p,c,a & LIN p,c,p ) by DIRAF:36, DIRAF:37;
hence contradiction by A4, A5, A6, DIRAF:38; :: thesis: verum

end;

A34: a <> e2

proof

assume A35: a = e2 ; :: thesis: contradiction
e1,a // a,c by A12, DIRAF:5;
then b,c // a,c by A17, A32, A35, DIRAF:6;
then c,b // c,a by DIRAF:5;
then ( Mid c,b,a or Mid c,a,b ) by DIRAF:11;
then ( LIN c,b,a or LIN c,a,b ) by DIRAF:34;
then ( LIN c,b,a & LIN c,b,p & LIN c,b,b ) by A6, DIRAF:36, DIRAF:37;
hence contradiction by A4, A10, DIRAF:38; :: thesis: verum

end;

d,e2 // d,e3 by A28, ANALOAF:def 5;
then d,e1 // d,e3 by A27, A30, DIRAF:6;
then ( Mid d,e1,e3 or Mid d,e3,e1 ) by DIRAF:11;
then ( LIN d,e1,e3 or LIN d,e3,e1 ) by DIRAF:34;
then ( LIN d,e3,e1 & LIN c,e1,a ) by A15, DIRAF:36;
then A36: LIN d,e3,a by A21, A24, DIRAF:41;
LIN d,e3,e2 by A29, DIRAF:36;
then A37: LIN d,e3,b by A18, A34, A36, DIRAF:41;
LIN c,b,p by A6, DIRAF:36;
then LIN d,e3,p by A10, A24, A37, DIRAF:41;
hence contradiction by A4, A31, A36, A37, DIRAF:38; :: thesis: verum

end;

now

assume b = c ; :: thesis: a = d
then ( Mid b,d,a or Mid b,a,d ) by A2, DIRAF:11;
then ( LIN b,d,a or LIN b,a,d ) by DIRAF:34;
then ( LIN d,a,b & LIN d,a,p & LIN d,a,a ) by A8, DIRAF:36, DIRAF:37;
hence a = d by A4, DIRAF:38; :: thesis: verum

end;

hence Mid p,d,a by A9, DIRAF:14; :: thesis: verum

end;

hence Mid p,d,a by A3, DIRAF:11; :: thesis: verum