let OAS be OAffinSpace; :: thesis: for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid a,x,c & not a,b,c are_collinear holds

ex y being Element of OAS st

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

let a, b, c, d, x be Element of OAS; :: thesis: ( Mid a,b,d & Mid a,x,c & not a,b,c are_collinear implies ex y being Element of OAS st

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

assume that

A1: Mid a,b,d and

A2: Mid a,x,c and

A3: not a,b,c are_collinear ; :: thesis: ex y being Element of OAS st

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

A4: b <> c by A3, DIRAF:31;

A5: a <> b by A3, DIRAF:31;

A78: ( x = c implies ( Mid b,c,c & Mid x,c,d ) ) by DIRAF:10;

( a = x implies ( Mid b,b,c & Mid x,b,d ) ) by A1, DIRAF:10;

hence ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) by A6, A77, A78; :: thesis: verum

ex y being Element of OAS st

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

let a, b, c, d, x be Element of OAS; :: thesis: ( Mid a,b,d & Mid a,x,c & not a,b,c are_collinear implies ex y being Element of OAS st

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

assume that

A1: Mid a,b,d and

A2: Mid a,x,c and

A3: not a,b,c are_collinear ; :: thesis: ex y being Element of OAS st

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

A4: b <> c by A3, DIRAF:31;

A5: a <> b by A3, DIRAF:31;

A6: now :: thesis: ( b <> d & x <> c & a <> x implies ex y being Element of OAS st

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

A77:
( b = d implies ( Mid b,d,c & Mid x,d,d ) )
by DIRAF:10;( Mid b,y,c & Mid x,y,d ) )

assume that

A7: b <> d and

A8: x <> c and

A9: a <> x ; :: thesis: ex y being Element of OAS st

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

A10: a <> d by A1, A7, DIRAF:8;

consider e1 being Element of OAS such that

A11: Mid a,d,e1 and

A12: x,d // c,e1 by A2, A9, Th20;

A13: Mid e1,d,a by A11, DIRAF:9;

A14: d,b,a are_collinear by A1, DIRAF:9, DIRAF:28;

A15: not a,x,b are_collinear

A22: Mid d,b,a by A1, DIRAF:9;

Mid b,d,e1 by A1, A11, DIRAF:11;

then Mid e1,d,b by DIRAF:9;

then Mid e1,b,a by A22, A13, DIRAF:12;

then A23: e1,b // b,a by DIRAF:def 3;

e1 <> b by A7, A22, A13, DIRAF:14;

then consider e2 being Element of OAS such that

A24: c,b // b,e2 and

A25: c,e1 // a,e2 by A23, ANALOAF:def 5;

A26: Mid c,b,e2 by A24, DIRAF:def 3;

then A27: c,b,e2 are_collinear by DIRAF:28;

Mid c,x,a by A2, DIRAF:9;

then consider y being Element of OAS such that

A28: Mid c,y,e2 and

A29: a,e2 // x,y by Th19;

A30: ( Mid c,b,y or Mid c,y,b ) by A26, A28, DIRAF:17;

A31: c <> e2 by A4, A24, ANALOAF:def 5;

A50: c <> e1

then x,d // x,y by A48, A29, DIRAF:3;

then A53: ( Mid x,d,y or Mid x,y,d ) by DIRAF:7;

then A54: Mid d,y,x by A32, DIRAF:9;

hence ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) by A53, A32; :: thesis: verum

end;A7: b <> d and

A8: x <> c and

A9: a <> x ; :: thesis: ex y being Element of OAS st

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

A10: a <> d by A1, A7, DIRAF:8;

consider e1 being Element of OAS such that

A11: Mid a,d,e1 and

A12: x,d // c,e1 by A2, A9, Th20;

A13: Mid e1,d,a by A11, DIRAF:9;

A14: d,b,a are_collinear by A1, DIRAF:9, DIRAF:28;

A15: not a,x,b are_collinear

proof

A18:
not x,d,a are_collinear
A16:
a,x,a are_collinear
by DIRAF:31;

assume A17: a,x,b are_collinear ; :: thesis: contradiction

a,x,c are_collinear by A2, DIRAF:28;

hence contradiction by A3, A9, A17, A16, DIRAF:32; :: thesis: verum

end;assume A17: a,x,b are_collinear ; :: thesis: contradiction

a,x,c are_collinear by A2, DIRAF:28;

hence contradiction by A3, A9, A17, A16, DIRAF:32; :: thesis: verum

proof

then A21:
x <> d
by DIRAF:31;
assume
x,d,a are_collinear
; :: thesis: contradiction

then A19: d,a,x are_collinear by DIRAF:30;

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

d,a,b are_collinear by A14, DIRAF:30;

hence contradiction by A10, A15, A19, A20, DIRAF:32; :: thesis: verum

end;then A19: d,a,x are_collinear by DIRAF:30;

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

d,a,b are_collinear by A14, DIRAF:30;

hence contradiction by A10, A15, A19, A20, DIRAF:32; :: thesis: verum

A22: Mid d,b,a by A1, DIRAF:9;

Mid b,d,e1 by A1, A11, DIRAF:11;

then Mid e1,d,b by DIRAF:9;

then Mid e1,b,a by A22, A13, DIRAF:12;

then A23: e1,b // b,a by DIRAF:def 3;

e1 <> b by A7, A22, A13, DIRAF:14;

then consider e2 being Element of OAS such that

A24: c,b // b,e2 and

A25: c,e1 // a,e2 by A23, ANALOAF:def 5;

A26: Mid c,b,e2 by A24, DIRAF:def 3;

then A27: c,b,e2 are_collinear by DIRAF:28;

Mid c,x,a by A2, DIRAF:9;

then consider y being Element of OAS such that

A28: Mid c,y,e2 and

A29: a,e2 // x,y by Th19;

A30: ( Mid c,b,y or Mid c,y,b ) by A26, A28, DIRAF:17;

A31: c <> e2 by A4, A24, ANALOAF:def 5;

A32: now :: thesis: not Mid x,d,y

A48:
a <> e2
c,b,e2 are_collinear
by A26, DIRAF:28;

then A33: c,e2,b are_collinear by DIRAF:30;

c,y,e2 are_collinear by A28, DIRAF:28;

then A34: c,e2,y are_collinear by DIRAF:30;

c,e2,c are_collinear by DIRAF:31;

then A35: b,y,c are_collinear by A31, A34, A33, DIRAF:32;

a,x,c are_collinear by A2, DIRAF:28;

then A36: x,a,c are_collinear by DIRAF:30;

A37: Mid c,x,a by A2, DIRAF:9;

assume A38: Mid x,d,y ; :: thesis: contradiction

then consider c9 being Element of OAS such that

A39: Mid x,c9,a and

A40: Mid c9,b,y by A22, A18, Th27;

x,c9,a are_collinear by A39, DIRAF:28;

then A41: x,a,c9 are_collinear by DIRAF:30;

A42: b <> y

then A45: b,y,c9 are_collinear by DIRAF:30;

then A46: c,c9,c are_collinear by A42, A35, DIRAF:32;

b,y,b are_collinear by DIRAF:31;

then A47: c,c9,b are_collinear by A42, A35, A45, DIRAF:32;

x,a,a are_collinear by DIRAF:31;

then c,c9,a are_collinear by A9, A36, A41, DIRAF:32;

then Mid x,c,a by A3, A39, A47, A46, DIRAF:32;

hence contradiction by A8, A37, DIRAF:14; :: thesis: verum

end;then A33: c,e2,b are_collinear by DIRAF:30;

c,y,e2 are_collinear by A28, DIRAF:28;

then A34: c,e2,y are_collinear by DIRAF:30;

c,e2,c are_collinear by DIRAF:31;

then A35: b,y,c are_collinear by A31, A34, A33, DIRAF:32;

a,x,c are_collinear by A2, DIRAF:28;

then A36: x,a,c are_collinear by DIRAF:30;

A37: Mid c,x,a by A2, DIRAF:9;

assume A38: Mid x,d,y ; :: thesis: contradiction

then consider c9 being Element of OAS such that

A39: Mid x,c9,a and

A40: Mid c9,b,y by A22, A18, Th27;

x,c9,a are_collinear by A39, DIRAF:28;

then A41: x,a,c9 are_collinear by DIRAF:30;

A42: b <> y

proof

c9,b,y are_collinear
by A40, DIRAF:28;
assume
b = y
; :: thesis: contradiction

then x,d,b are_collinear by A38, DIRAF:28;

then A43: d,b,x are_collinear by DIRAF:30;

A44: d,b,b are_collinear by DIRAF:31;

a,x,c are_collinear by A2, DIRAF:28;

then d,b,c are_collinear by A9, A14, A43, DIRAF:35;

hence contradiction by A3, A7, A14, A44, DIRAF:32; :: thesis: verum

end;then x,d,b are_collinear by A38, DIRAF:28;

then A43: d,b,x are_collinear by DIRAF:30;

A44: d,b,b are_collinear by DIRAF:31;

a,x,c are_collinear by A2, DIRAF:28;

then d,b,c are_collinear by A9, A14, A43, DIRAF:35;

hence contradiction by A3, A7, A14, A44, DIRAF:32; :: thesis: verum

then A45: b,y,c9 are_collinear by DIRAF:30;

then A46: c,c9,c are_collinear by A42, A35, DIRAF:32;

b,y,b are_collinear by DIRAF:31;

then A47: c,c9,b are_collinear by A42, A35, A45, DIRAF:32;

x,a,a are_collinear by DIRAF:31;

then c,c9,a are_collinear by A9, A36, A41, DIRAF:32;

then Mid x,c,a by A3, A39, A47, A46, DIRAF:32;

hence contradiction by A8, A37, DIRAF:14; :: thesis: verum

proof

A49:
e1,d,a are_collinear
by A11, DIRAF:9, DIRAF:28;
assume
a = e2
; :: thesis: contradiction

then Mid c,b,a by A24, DIRAF:def 3;

hence contradiction by A3, DIRAF:9, DIRAF:28; :: thesis: verum

end;then Mid c,b,a by A24, DIRAF:def 3;

hence contradiction by A3, DIRAF:9, DIRAF:28; :: thesis: verum

A50: c <> e1

proof

then
x,d // a,e2
by A12, A25, DIRAF:3;
assume
c = e1
; :: thesis: contradiction

then A51: d,a,c are_collinear by A49, DIRAF:30;

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

d,a,b are_collinear by A14, DIRAF:30;

hence contradiction by A3, A10, A51, A52, DIRAF:32; :: thesis: verum

end;then A51: d,a,c are_collinear by A49, DIRAF:30;

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

d,a,b are_collinear by A14, DIRAF:30;

hence contradiction by A3, A10, A51, A52, DIRAF:32; :: thesis: verum

then x,d // x,y by A48, A29, DIRAF:3;

then A53: ( Mid x,d,y or Mid x,y,d ) by DIRAF:7;

then A54: Mid d,y,x by A32, DIRAF:9;

now :: thesis: Mid c,y,b

then
Mid b,y,c
by DIRAF:9;A55:
b <> e2

A62: y <> d

assume A66: not Mid c,y,b ; :: thesis: contradiction

then A67: y <> b by DIRAF:10;

Mid b,y,e2 by A28, A30, A66, DIRAF:11;

then consider z being Element of OAS such that

A68: Mid b,d,z and

A69: y,d // e2,z by A67, Th20;

A70: a,e2,a are_collinear by DIRAF:31;

then d,y // d,x by ANALOAF:def 5;

then y,d // x,d by DIRAF:2;

then y,d // c,e1 by A12, A21, DIRAF:3;

then c,e1 // e2,z by A69, A62, ANALOAF:def 5;

then a,e2 // e2,z by A25, A50, ANALOAF:def 5;

then Mid a,e2,z by DIRAF:def 3;

then a,e2,z are_collinear by DIRAF:28;

then A73: a,z,e2 are_collinear by DIRAF:30;

A74: b,d,z are_collinear by A68, DIRAF:28;

then A75: a,z,a are_collinear by A7, A61, DIRAF:32;

b,d,b are_collinear by DIRAF:31;

then a,z,b are_collinear by A7, A74, A61, DIRAF:32;

then A76: a,e2,b are_collinear by A73, A75, A71, DIRAF:32;

a,e2,e2 are_collinear by A73, A75, A71, DIRAF:32;

then a,e2,c are_collinear by A55, A76, A65, DIRAF:35;

hence contradiction by A3, A48, A76, A70, DIRAF:32; :: thesis: verum

end;proof

A61:
b,d,a are_collinear
by A14, DIRAF:30;
A56:
a,b // b,d
by A1, DIRAF:def 3;

assume A57: b = e2 ; :: thesis: contradiction

c,e1 // x,d by A12, DIRAF:2;

then a,b // x,d by A25, A50, A57, ANALOAF:def 5;

then x,d // b,d by A5, A56, ANALOAF:def 5;

then d,x // d,b by DIRAF:2;

then ( Mid d,x,b or Mid d,b,x ) by DIRAF:7;

then ( d,x,b are_collinear or d,b,x are_collinear ) by DIRAF:28;

then A58: d,b,x are_collinear by DIRAF:30;

d,b,b are_collinear by DIRAF:31;

then A59: a,x,b are_collinear by A7, A14, A58, DIRAF:32;

A60: a,x,c are_collinear by A2, DIRAF:28;

a,x,a are_collinear by A7, A14, A58, DIRAF:32;

hence contradiction by A3, A9, A59, A60, DIRAF:32; :: thesis: verum

end;assume A57: b = e2 ; :: thesis: contradiction

c,e1 // x,d by A12, DIRAF:2;

then a,b // x,d by A25, A50, A57, ANALOAF:def 5;

then x,d // b,d by A5, A56, ANALOAF:def 5;

then d,x // d,b by DIRAF:2;

then ( Mid d,x,b or Mid d,b,x ) by DIRAF:7;

then ( d,x,b are_collinear or d,b,x are_collinear ) by DIRAF:28;

then A58: d,b,x are_collinear by DIRAF:30;

d,b,b are_collinear by DIRAF:31;

then A59: a,x,b are_collinear by A7, A14, A58, DIRAF:32;

A60: a,x,c are_collinear by A2, DIRAF:28;

a,x,a are_collinear by A7, A14, A58, DIRAF:32;

hence contradiction by A3, A9, A59, A60, DIRAF:32; :: thesis: verum

A62: y <> d

proof

A65:
b,e2,c are_collinear
by A27, DIRAF:30;
A63:
c,e2,c are_collinear
by DIRAF:31;

A64: c,e2,b are_collinear by A27, DIRAF:30;

assume y = d ; :: thesis: contradiction

then c,d,e2 are_collinear by A28, DIRAF:28;

then c,e2,d are_collinear by DIRAF:30;

then c,e2,a are_collinear by A7, A14, A64, DIRAF:35;

hence contradiction by A3, A31, A64, A63, DIRAF:32; :: thesis: verum

end;A64: c,e2,b are_collinear by A27, DIRAF:30;

assume y = d ; :: thesis: contradiction

then c,d,e2 are_collinear by A28, DIRAF:28;

then c,e2,d are_collinear by DIRAF:30;

then c,e2,a are_collinear by A7, A14, A64, DIRAF:35;

hence contradiction by A3, A31, A64, A63, DIRAF:32; :: thesis: verum

assume A66: not Mid c,y,b ; :: thesis: contradiction

then A67: y <> b by DIRAF:10;

Mid b,y,e2 by A28, A30, A66, DIRAF:11;

then consider z being Element of OAS such that

A68: Mid b,d,z and

A69: y,d // e2,z by A67, Th20;

A70: a,e2,a are_collinear by DIRAF:31;

A71: now :: thesis: not a = z

d,y // y,x
by A54, DIRAF:def 3;assume A72:
a = z
; :: thesis: contradiction

Mid d,b,a by A1, DIRAF:9;

hence contradiction by A7, A68, A72, DIRAF:14; :: thesis: verum

end;Mid d,b,a by A1, DIRAF:9;

hence contradiction by A7, A68, A72, DIRAF:14; :: thesis: verum

then d,y // d,x by ANALOAF:def 5;

then y,d // x,d by DIRAF:2;

then y,d // c,e1 by A12, A21, DIRAF:3;

then c,e1 // e2,z by A69, A62, ANALOAF:def 5;

then a,e2 // e2,z by A25, A50, ANALOAF:def 5;

then Mid a,e2,z by DIRAF:def 3;

then a,e2,z are_collinear by DIRAF:28;

then A73: a,z,e2 are_collinear by DIRAF:30;

A74: b,d,z are_collinear by A68, DIRAF:28;

then A75: a,z,a are_collinear by A7, A61, DIRAF:32;

b,d,b are_collinear by DIRAF:31;

then a,z,b are_collinear by A7, A74, A61, DIRAF:32;

then A76: a,e2,b are_collinear by A73, A75, A71, DIRAF:32;

a,e2,e2 are_collinear by A73, A75, A71, DIRAF:32;

then a,e2,c are_collinear by A55, A76, A65, DIRAF:35;

hence contradiction by A3, A48, A76, A70, DIRAF:32; :: thesis: verum

hence ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) by A53, A32; :: thesis: verum

A78: ( x = c implies ( Mid b,c,c & Mid x,c,d ) ) by DIRAF:10;

( a = x implies ( Mid b,b,c & Mid x,b,d ) ) by A1, DIRAF:10;

hence ex y being Element of OAS st

( Mid b,y,c & Mid x,y,d ) by A6, A77, A78; :: thesis: verum