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

A8: now

A9: p <> a by A4, DIRAF:37;
assume that
A10: b <> c and
A11: d <> a ; :: thesis: Mid p,d,a
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 A9, ANALOAF:def 5;
A14: d,e1 // c,p by A13, DIRAF:5;
A15: 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;

Mid b,c,p by A1, DIRAF:13;
then A16: b,c // c,p by DIRAF:def 3;
then A17: c,p // b,c by DIRAF:5;
consider e2 being Element of OAS such that
A18: b,a // a,e2 and
A19: b,c // e1,e2 by A4, A6, A12, ANALOAF:def 5;
consider e3 being Element of OAS such that
A20: b,c // e2,e3 and
A21: b,e2 // c,e3 and
c <> e3 by ANALOAF:def 5;
A22: a <> b by A4, DIRAF:37;
A23: Mid c,a,e1 by A12, DIRAF:def 3;
A24: d <> e1

proof

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

end;

b,a // b,e2 by A18, ANALOAF:def 5;
then A27: c,d // b,e2 by A2, A22, DIRAF:6;
b <> e2 by A22, A18, ANALOAF:def 5;
then c,d // c,e3 by A21, A27, 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;
then A28: LIN d,e3,c by DIRAF:36;
e1,e2 // c,p by A10, A19, A16, ANALOAF:def 5;
then A29: e1,e2 // d,e1 by A5, A13, DIRAF:6;
then d,e1 // e1,e2 by DIRAF:5;
then A30: d,e1 // d,e2 by ANALOAF:def 5;
then d,e2 // d,e1 by DIRAF:5;
then d,e2 // c,p by A24, A14, DIRAF:6;
then d,e2 // b,c by A5, A17, DIRAF:6;
then A31: d,e2 // e2,e3 by A10, A20, DIRAF:6;
then Mid d,e2,e3 by DIRAF:def 3;
then LIN d,e2,e3 by DIRAF:34;
then A32: LIN d,e3,e2 by DIRAF:36;
A33: d <> e2 by A24, A29, ANALOAF:def 5;
then A34: d <> e3 by A31, ANALOAF:def 5;
d,e2 // d,e3 by A31, ANALOAF:def 5;
then d,e1 // d,e3 by A30, A33, 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 A35: LIN d,e3,e1 by DIRAF:36;
LIN c,a,e1 by A23, DIRAF:34;
then LIN c,e1,a by DIRAF:36;
then A36: LIN d,e3,a by A15, A28, A35, DIRAF:41;
A37: a <> e1

proof

p,a // a,d by A7, DIRAF:def 3;
then A38: d,a // a,p by DIRAF:5;
assume a = e1 ; :: thesis: contradiction
then c,p // a,p by A11, A13, A38, 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 A39: LIN p,c,a by DIRAF:36;
LIN p,c,p by DIRAF:37;
hence contradiction by A4, A5, A6, A39, DIRAF:38; :: thesis: verum

end;

A40: a <> e2

proof

assume A41: a = e2 ; :: thesis: contradiction
e1,a // a,c by A12, DIRAF:5;
then b,c // a,c by A19, A37, A41, 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 A42: LIN c,b,a by DIRAF:36;
A43: LIN c,b,b by DIRAF:37;
LIN c,b,p by A6, DIRAF:36;
hence contradiction by A4, A10, A42, A43, DIRAF:38; :: thesis: verum

end;

Mid b,a,e2 by A18, DIRAF:def 3;
then LIN b,a,e2 by DIRAF:34;
then LIN a,e2,b by DIRAF:36;
then A44: LIN d,e3,b by A40, A36, A32, DIRAF:41;
LIN c,b,p by A6, DIRAF:36;
then LIN d,e3,p by A10, A28, A44, DIRAF:41;
hence contradiction by A4, A34, A36, A44, DIRAF:38; :: thesis: verum

end;

A45: LIN p,a,d by A7, DIRAF:34;

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 A46: LIN d,a,b by DIRAF:36;
A47: LIN d,a,a by DIRAF:37;
LIN d,a,p by A45, DIRAF:36;
hence a = d by A4, A46, A47, DIRAF:38; :: thesis: verum

end;

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

end;

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