let OAS be OAffinSpace; :: thesis: for a, b, c, d, p being Element of OAS st Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p <> c holds
Mid p,d,a
let a, b, c, d, p be Element of OAS; :: thesis: ( Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & 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 p,a,b are_collinear and
A5: p <> c ; :: thesis: Mid p,d,a
A6: p,c,b are_collinear by A1, DIRAF:28;

now :: thesis: ( Mid p,a,d implies Mid p,d,a )

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

A8: now :: thesis: ( b <> c & d <> a implies Mid p,d,a )

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 by A12, DIRAF:def 3, A4, A6, DIRAF:8;
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 ( p,d,a are_collinear or p,a,d are_collinear ) by DIRAF:28;
then A25: d,a,p are_collinear by DIRAF:30;
A26: d,a,a are_collinear by DIRAF:31;
assume d = e1 ; :: thesis: contradiction
then c,a,d are_collinear by A23, DIRAF:28;
then d,a,c are_collinear by DIRAF:30;
then d,a,b are_collinear 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 ( c,d,e3 are_collinear or c,e3,d are_collinear ) by DIRAF:28;
then A28: d,e3,c are_collinear 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 d,e2,e3 are_collinear by DIRAF:28;
then A32: d,e3,e2 are_collinear 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 ( d,e1,e3 are_collinear or d,e3,e1 are_collinear ) by DIRAF:28;
then A35: d,e3,e1 are_collinear by DIRAF:30;
c,a,e1 are_collinear by A23, DIRAF:28;
then c,e1,a are_collinear by DIRAF:30;
then A36: d,e3,a are_collinear 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 ( p,c,a are_collinear or p,a,c are_collinear ) by DIRAF:28;
then A39: p,c,a are_collinear by DIRAF:30;
p,c,p are_collinear 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 ( c,b,a are_collinear or c,a,b are_collinear ) by DIRAF:28;
then A42: c,b,a are_collinear by DIRAF:30;
A43: c,b,b are_collinear by DIRAF:31;
c,b,p are_collinear 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 b,a,e2 are_collinear by DIRAF:28;
then a,e2,b are_collinear by DIRAF:30;
then A44: d,e3,b are_collinear by A40, A36, A32, DIRAF:35;
c,b,p are_collinear by A6, DIRAF:30;
then d,e3,p are_collinear by A10, A28, A44, DIRAF:35;
hence contradiction by A4, A34, A36, A44, DIRAF:32; :: thesis: verum

end;

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

now :: thesis: ( b = c implies a = d )

assume b = c ; :: thesis: a = d
then ( Mid b,d,a or Mid b,a,d ) by A2, DIRAF:7;
then ( b,d,a are_collinear or b,a,d are_collinear ) by DIRAF:28;
then A46: d,a,b are_collinear by DIRAF:30;
A47: d,a,a are_collinear by DIRAF:31;
d,a,p are_collinear 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