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 )

( Mid a,x,d & Mid b,x,c ) by A3; :: thesis: verum

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 ) )

( 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

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

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

A25: c <> e1

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

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

A10:
not a,b,d are_collinear
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;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

proof

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 A11: now :: thesis: ( a,b // a,d implies d,c,a are_collinear )

A12:
d,a,a are_collinear
by DIRAF:31;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;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

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

assume A14:
a,b,d are_collinear
; :: thesis: contradictionassume
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;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

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

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

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;A22: now :: thesis: not c,d // c,b

assume
c,d,b are_collinear
; :: thesis: contradictionassume
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;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

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

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

A25: c <> e1

proof

not c,b,e1 are_collinear
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;then c,d // d,c by A1, A4, A7, ANALOAF:def 5;

hence contradiction by A19, ANALOAF:def 5; :: thesis: verum

proof

then consider x being Element of OAS such that
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 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

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

not a,d,e2 are_collinear
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;then a,b // b,a by A1, A19, A16, DIRAF:3;

hence contradiction by A7, ANALOAF:def 5; :: thesis: verum

proof

then consider y being Element of OAS such that
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 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

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

now :: thesis: ( c = d implies ex x being Element of OAS st

( Mid a,x,d & Mid b,x,c ) )

hence
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;( 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

( Mid a,x,d & Mid b,x,c ) by A3; :: thesis: verum