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:28;

now

assume A7: Mid p,a,d ; :: thesis: Mid p,d,a

A8: now

A9: p <> a by A4, DIRAF:31;
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:7;
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:2;
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:8; :: thesis: verum

end;

Mid b,c,p by A1, DIRAF:9;
then A16: b,c // c,p by DIRAF:def 3;
then A17: c,p // b,c by DIRAF:2;
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:31;
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:7;
then ( LIN p,d,a or LIN p,a,d ) by DIRAF:28;
then A25: LIN d,a,p by DIRAF:30;
A26: LIN d,a,a by DIRAF:31;
assume d = e1 ; :: thesis: contradiction
then LIN c,a,d by A23, DIRAF:28;
then LIN d,a,c by DIRAF:30;
then LIN d,a,b by A5, A6, A25, DIRAF:35;
hence contradiction by A4, A11, A25, A26, DIRAF:32; :: thesis: verum

end;

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

proof

p,a // a,d by A7, DIRAF:def 3;
then A38: d,a // a,p by DIRAF:2;
assume a = e1 ; :: thesis: contradiction
then c,p // a,p by A11, A13, A38, DIRAF:3;
then p,c // p,a by DIRAF:2;
then ( Mid p,c,a or Mid p,a,c ) by DIRAF:7;
then ( LIN p,c,a or LIN p,a,c ) by DIRAF:28;
then A39: LIN p,c,a by DIRAF:30;
LIN p,c,p by DIRAF:31;
hence contradiction by A4, A5, A6, A39, DIRAF:32; :: thesis: verum

end;

A40: a <> e2

proof

assume A41: a = e2 ; :: thesis: contradiction
e1,a // a,c by A12, DIRAF:2;
then b,c // a,c by A19, A37, A41, DIRAF:3;
then c,b // c,a by DIRAF:2;
then ( Mid c,b,a or Mid c,a,b ) by DIRAF:7;
then ( LIN c,b,a or LIN c,a,b ) by DIRAF:28;
then A42: LIN c,b,a by DIRAF:30;
A43: LIN c,b,b by DIRAF:31;
LIN c,b,p by A6, DIRAF:30;
hence contradiction by A4, A10, A42, A43, DIRAF:32; :: thesis: verum

end;

Mid b,a,e2 by A18, DIRAF:def 3;
then LIN b,a,e2 by DIRAF:28;
then LIN a,e2,b by DIRAF:30;
then A44: LIN d,e3,b by A40, A36, A32, DIRAF:35;
LIN c,b,p by A6, DIRAF:30;
then LIN d,e3,p by A10, A28, A44, DIRAF:35;
hence contradiction by A4, A34, A36, A44, DIRAF:32; :: thesis: verum

end;

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

now

assume b = c ; :: thesis: a = d
then ( Mid b,d,a or Mid b,a,d ) by A2, DIRAF:7;
then ( LIN b,d,a or LIN b,a,d ) by DIRAF:28;
then A46: LIN d,a,b by DIRAF:30;
A47: LIN d,a,a by DIRAF:31;
LIN d,a,p by A45, DIRAF:30;
hence a = d by A4, A46, A47, DIRAF:32; :: thesis: verum

end;

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

end;

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