let OAS be OAffinSpace; :: thesis: for a, b, c, d being Element of OAS st a,b // c,d & not a,b,c are_collinear holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
let a, b, c, d be Element of OAS; :: thesis: ( a,b // c,d & not a,b,c are_collinear implies ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) )
assume that
A1: a,b // c,d and
A2: not a,b,c are_collinear ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )

A3: now :: thesis: ( c <> d implies ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) )

consider e1 being Element of OAS such that
A4: a,b // d,e1 and
A5: a,d // b,e1 and
A6: b <> e1 by ANALOAF:def 5;
A7: a <> b by A2, DIRAF:31;
then c,d // d,e1 by A1, A4, ANALOAF:def 5;
then A8: Mid c,d,e1 by DIRAF:def 3;
A9: a <> d

proof

assume a = d ; :: thesis: contradiction
then b,a // a,c by A1, DIRAF:2;
then Mid b,a,c by DIRAF:def 3;
then b,a,c are_collinear by DIRAF:28;
hence contradiction by A2, DIRAF:30; :: thesis: verum

end;

A10: not a,b,d are_collinear

proof

A11: now :: thesis: ( a,b // a,d implies d,c,a are_collinear )

assume a,b // a,d ; :: thesis: d,c,a are_collinear
then c,d // a,d by A1, A7, ANALOAF:def 5;
then d,c // d,a by DIRAF:2;
then d,c '||' d,a by DIRAF:def 4;
hence d,c,a are_collinear by DIRAF:def 5; :: thesis: verum

end;

A12: d,a,a are_collinear by DIRAF:31;

A13: now :: thesis: ( a,b // d,a implies d,c,a are_collinear )

assume a,b // d,a ; :: thesis: d,c,a are_collinear
then c,d // d,a by A1, A7, ANALOAF:def 5;
then Mid c,d,a by DIRAF:def 3;
then c,d,a are_collinear by DIRAF:28;
hence d,c,a are_collinear by DIRAF:30; :: thesis: verum

end;

assume A14: a,b,d are_collinear ; :: thesis: contradiction
then A15: d,a,b are_collinear by DIRAF:30;
a,b '||' a,d by A14, DIRAF:def 5;
then d,a,c are_collinear by A11, A13, DIRAF:30, DIRAF:def 4;
hence contradiction by A2, A9, A12, A15, DIRAF:32; :: thesis: verum

end;

consider e2 being Element of OAS such that
A16: c,d // b,e2 and
A17: c,b // d,e2 and
A18: d <> e2 by ANALOAF:def 5;
assume A19: c <> d ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
then a,b // b,e2 by A1, A16, DIRAF:3;
then A20: Mid a,b,e2 by DIRAF:def 3;
A21: not c,d,b are_collinear

proof

A22: now :: thesis: not c,d // c,b

assume c,d // c,b ; :: thesis: contradiction
then a,b // c,b by A1, A19, DIRAF:3;
then b,a // b,c by DIRAF:2;
then ( Mid b,a,c or Mid b,c,a ) by DIRAF:7;
then ( b,a,c are_collinear or b,c,a are_collinear ) by DIRAF:28;
hence contradiction by A2, DIRAF:30; :: thesis: verum

end;

assume c,d,b are_collinear ; :: thesis: contradiction
then c,d '||' c,b by DIRAF:def 5;
then ( c,d // c,b or c,d // b,c ) by DIRAF:def 4;
then a,b // b,c by A1, A19, A22, DIRAF:3;
then Mid a,b,c by DIRAF:def 3;
hence contradiction by A2, DIRAF:28; :: thesis: verum

end;

A23: b,c,c are_collinear by DIRAF:31;
A24: d,a,a are_collinear by DIRAF:31;
A25: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then c,d // d,c by A1, A4, A7, ANALOAF:def 5;
hence contradiction by A19, ANALOAF:def 5; :: thesis: verum

end;

not c,b,e1 are_collinear

proof

c,d,e1 are_collinear by A8, DIRAF:28;
then A26: c,e1,d are_collinear by DIRAF:30;
assume c,b,e1 are_collinear ; :: thesis: contradiction
then A27: c,e1,b are_collinear by DIRAF:30;
c,e1,c are_collinear by DIRAF:31;
hence contradiction by A25, A21, A27, A26, DIRAF:32; :: thesis: verum

end;

then consider x being Element of OAS such that
A28: Mid c,x,b and
A29: b,e1 // x,d by A8, Th21;
A30: Mid b,x,c by A28, DIRAF:9;
a,d // x,d by A5, A6, A29, DIRAF:3;
then d,a // d,x by DIRAF:2;
then ( Mid d,a,x or Mid d,x,a ) by DIRAF:7;
then ( d,a,x are_collinear or d,x,a are_collinear ) by DIRAF:28;
then A31: d,a,x are_collinear by DIRAF:30;
A32: b <> c by A2, DIRAF:31;
A33: a <> e2

proof

assume a = e2 ; :: thesis: contradiction
then a,b // b,a by A1, A19, A16, DIRAF:3;
hence contradiction by A7, ANALOAF:def 5; :: thesis: verum

end;

not a,d,e2 are_collinear

proof

a,b,e2 are_collinear by A20, DIRAF:28;
then A34: a,e2,b are_collinear by DIRAF:30;
assume a,d,e2 are_collinear ; :: thesis: contradiction
then A35: a,e2,d are_collinear by DIRAF:30;
a,e2,a are_collinear by DIRAF:31;
hence contradiction by A33, A10, A35, A34, DIRAF:32; :: thesis: verum

end;

then consider y being Element of OAS such that
A36: Mid a,y,d and
A37: d,e2 // y,b by A20, Th21;
A38: b,c,b are_collinear by DIRAF:31;
c,b // y,b by A17, A18, A37, DIRAF:3;
then b,c // b,y by DIRAF:2;
then ( Mid b,c,y or Mid b,y,c ) by DIRAF:7;
then ( b,c,y are_collinear or b,y,c are_collinear ) by DIRAF:28;
then A39: b,c,y are_collinear by DIRAF:30;
A40: c,x,b are_collinear by A28, DIRAF:28;
then b,c,x are_collinear by DIRAF:30;
then A41: x,y,c are_collinear by A32, A39, A23, DIRAF:32;
a,y,d are_collinear by A36, DIRAF:28;
then d,a,y are_collinear by DIRAF:30;
then A42: x,y,a are_collinear by A9, A31, A24, DIRAF:32;
b,c,x are_collinear by A40, DIRAF:30;
then x,y,b are_collinear by A32, A39, A38, DIRAF:32;
then Mid a,x,d by A2, A36, A42, A41, DIRAF:32;
hence ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) by A30; :: thesis: verum

end;

now :: thesis: ( c = d implies ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) )

assume A43: c = d ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
take x = c; :: thesis: ( Mid a,x,d & Mid b,x,c )
thus ( Mid a,x,d & Mid b,x,c ) by A43, DIRAF:10; :: thesis: verum

end;

hence ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) by A3; :: thesis: verum