let OAS be OAffinSpace; for a, b, c, p being Element of OAS st not p,a,b are_collinear & Mid p,c,b holds
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
let a, b, c, p be Element of OAS; ( not p,a,b are_collinear & Mid p,c,b implies ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) )
assume that
A1:
not p,a,b are_collinear
and
A2:
Mid p,c,b
; ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
A3:
p <> a
by A1, DIRAF:31;
A4:
p,c,b are_collinear
by A2, DIRAF:28;
A5:
Mid b,c,p
by A2, DIRAF:9;
then A6:
b,c // c,p
by DIRAF:def 3;
A7:
a <> b
by A1, DIRAF:31;
A8:
now ( b <> c & a <> c & p <> c implies ex x being Element of OAS st
( Mid p,x,a & a,b // x,c ) )assume that A9:
b <> c
and A10:
a <> c
and A11:
p <> c
;
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )consider e1 being
Element of
OAS such that A12:
Mid b,
e1,
a
and A13:
p,
a // c,
e1
by A5, Th19;
A14:
not
p,
c,
a are_collinear
A16:
a <> e1
proof
assume
a = e1
;
contradiction
then
a,
p // a,
c
by A13, DIRAF:2;
then
(
Mid a,
p,
c or
Mid a,
c,
p )
by DIRAF:7;
then
(
a,
p,
c are_collinear or
a,
c,
p are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end; consider e4 being
Element of
OAS such that A17:
e1,
c // c,
e4
and A18:
e1,
b // p,
e4
by A6, A9, ANALOAF:def 5;
consider e2 being
Element of
OAS such that A19:
a,
c // c,
e2
and A20:
a,
b // p,
e2
by A6, A9, ANALOAF:def 5;
consider e3 being
Element of
OAS such that A21:
p,
c // c,
e3
and A22:
p,
a // e2,
e3
by A10, A19, ANALOAF:def 5;
A23:
not
a,
b,
c are_collinear
proof
assume
a,
b,
c are_collinear
;
contradiction
then A24:
b,
c,
a are_collinear
by DIRAF:30;
A25:
b,
c,
b are_collinear
by DIRAF:31;
b,
c,
p are_collinear
by A4, DIRAF:30;
hence
contradiction
by A1, A9, A24, A25, DIRAF:32;
verum
end; A26:
c <> e2
proof
assume A27:
c = e2
;
contradiction
p,
c // c,
b
by A6, DIRAF:2;
then
a,
b // c,
b
by A11, A20, A27, 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 A23, DIRAF:30;
verum
end; A28:
e2 <> e3
proof
assume
e2 = e3
;
contradiction
then
c,
e2 // p,
c
by A21, DIRAF:2;
then
a,
c // p,
c
by A19, A26, DIRAF:3;
then
c,
a // c,
p
by DIRAF:2;
then
(
Mid c,
a,
p or
Mid c,
p,
a )
by DIRAF:7;
then
(
c,
a,
p are_collinear or
c,
p,
a are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end; A29:
c <> e1
A30:
p <> e4
proof
assume
p = e4
;
contradiction
then
c,
e1 // p,
c
by A17, DIRAF:2;
then
p,
a // p,
c
by A13, A29, DIRAF:3;
then
(
Mid p,
a,
c or
Mid p,
c,
a )
by DIRAF:7;
then
(
p,
a,
c are_collinear or
p,
c,
a are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end;
Mid e1,
c,
e4
by A17, DIRAF:def 3;
then
Mid e4,
c,
e1
by DIRAF:9;
then A31:
e4,
c // c,
e1
by DIRAF:def 3;
c,
e1 // e2,
e3
by A3, A13, A22, ANALOAF:def 5;
then A32:
e4,
c // e2,
e3
by A29, A31, DIRAF:3;
A33:
e2 <> e4
proof
assume
e2 = e4
;
contradiction
then
c,
e2 // e1,
c
by A17, DIRAF:2;
then
a,
c // e1,
c
by A19, A26, DIRAF:3;
then
c,
e1 // c,
a
by DIRAF:2;
then
p,
a // c,
a
by A13, A29, DIRAF:3;
then
a,
p // a,
c
by DIRAF:2;
then
(
Mid a,
p,
c or
Mid a,
c,
p )
by DIRAF:7;
then
(
a,
p,
c are_collinear or
a,
c,
p are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end; A34:
c <> e3
proof
assume
c = e3
;
contradiction
then
c,
e2 // a,
p
by A22, DIRAF:2;
then
a,
c // a,
p
by A19, A26, DIRAF:3;
then
(
Mid a,
c,
p or
Mid a,
p,
c )
by DIRAF:7;
then
(
a,
c,
p are_collinear or
a,
p,
c are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end; A35:
p <> e3
by A11, A21, ANALOAF:def 5;
A36:
not
p,
e3,
e2 are_collinear
proof
p,
c // c,
b
by A2, DIRAF:def 3;
then A37:
p,
c // p,
b
by ANALOAF:def 5;
p,
c // p,
e3
by A21, ANALOAF:def 5;
then
p,
b // p,
e3
by A11, A37, ANALOAF:def 5;
then
(
Mid p,
b,
e3 or
Mid p,
e3,
b )
by DIRAF:7;
then
(
p,
b,
e3 are_collinear or
p,
e3,
b are_collinear )
by DIRAF:28;
then A38:
p,
e3,
b are_collinear
by DIRAF:30;
A39:
p,
e3,
p are_collinear
by DIRAF:31;
a,
c // a,
e2
by A19, ANALOAF:def 5;
then
(
Mid a,
c,
e2 or
Mid a,
e2,
c )
by DIRAF:7;
then
(
a,
c,
e2 are_collinear or
a,
e2,
c are_collinear )
by DIRAF:28;
then A40:
c,
e2,
a are_collinear
by DIRAF:30;
p,
c // p,
e3
by A21, ANALOAF:def 5;
then
(
Mid p,
c,
e3 or
Mid p,
e3,
c )
by DIRAF:7;
then
(
p,
c,
e3 are_collinear or
p,
e3,
c are_collinear )
by DIRAF:28;
then A41:
p,
e3,
c are_collinear
by DIRAF:30;
assume
p,
e3,
e2 are_collinear
;
contradiction
then
p,
e3,
a are_collinear
by A26, A41, A40, DIRAF:35;
hence
contradiction
by A1, A35, A38, A39, DIRAF:32;
verum
end; then A42:
not
e3,
e2,
p are_collinear
by DIRAF:30;
consider e5 being
Element of
OAS such that A43:
e4,
e2 // c,
e5
and A44:
e4,
c // e2,
e5
and A45:
e2 <> e5
by ANALOAF:def 5;
A46:
b <> e1
proof
p,
c // c,
b
by A2, DIRAF:def 3;
then A47:
c,
b // p,
c
by DIRAF:2;
assume
b = e1
;
contradiction
then
p,
a // p,
c
by A9, A13, A47, DIRAF:3;
then
(
Mid p,
a,
c or
Mid p,
c,
a )
by DIRAF:7;
then
(
p,
a,
c are_collinear or
p,
c,
a are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end; A48:
c <> e4
proof
assume A49:
c = e4
;
contradiction
p,
c // c,
b
by A2, DIRAF:def 3;
then
e1,
b // c,
b
by A11, A18, A49, DIRAF:3;
then
b,
e1 // b,
c
by DIRAF:2;
then
(
Mid b,
e1,
c or
Mid b,
c,
e1 )
by DIRAF:7;
then
(
b,
e1,
c are_collinear or
b,
c,
e1 are_collinear )
by DIRAF:28;
then A50:
b,
e1,
c are_collinear
by DIRAF:30;
A51:
b,
e1,
b are_collinear
by DIRAF:31;
b,
e1,
a are_collinear
by A12, DIRAF:28;
hence
contradiction
by A23, A46, A50, A51, DIRAF:32;
verum
end; A52:
c <> e5
proof
assume
c = e5
;
contradiction
then
c,
e4 // c,
e2
by A44, DIRAF:2;
then
e1,
c // c,
e2
by A17, A48, DIRAF:3;
then
c,
e2 // e1,
c
by DIRAF:2;
then
a,
c // e1,
c
by A19, A26, DIRAF:3;
then
c,
e1 // c,
a
by DIRAF:2;
then
p,
a // c,
a
by A13, A29, DIRAF:3;
then
a,
p // a,
c
by DIRAF:2;
then
(
Mid a,
p,
c or
Mid a,
c,
p )
by DIRAF:7;
then
(
a,
p,
c are_collinear or
a,
c,
p are_collinear )
by DIRAF:28;
hence
contradiction
by A14, DIRAF:30;
verum
end;
Mid a,
e1,
b
by A12, DIRAF:9;
then A53:
a,
e1 // e1,
b
by DIRAF:def 3;
then
a,
e1 // a,
b
by ANALOAF:def 5;
then
a,
b // e1,
b
by A16, A53, ANALOAF:def 5;
then
e1,
b // p,
e2
by A7, A20, ANALOAF:def 5;
then A54:
p,
e4 // p,
e2
by A18, A46, ANALOAF:def 5;
Mid p,
c,
e3
by A21, DIRAF:def 3;
then
Mid p,
e4,
e2
by A36, A32, A30, A54, Th16;
then A55:
p,
e4 // e4,
e2
by DIRAF:def 3;
then
p,
e4 // p,
e2
by ANALOAF:def 5;
then A56:
p,
e2 // e4,
e2
by A30, A55, ANALOAF:def 5;
then A57:
p,
e2 // c,
e5
by A43, A33, DIRAF:3;
p <> e2
then A58:
a,
b // e4,
e2
by A20, A56, DIRAF:3;
then A59:
a,
b // c,
e5
by A43, A33, DIRAF:3;
A60:
e5 <> e3
proof
assume
e5 = e3
;
contradiction
then
c,
e3 // a,
b
by A59, DIRAF:2;
then
p,
c // a,
b
by A21, A34, DIRAF:3;
then
c,
p // b,
a
by DIRAF:2;
then
b,
c // b,
a
by A6, A11, DIRAF:3;
then
(
Mid b,
c,
a or
Mid b,
a,
c )
by DIRAF:7;
then
(
b,
c,
a are_collinear or
b,
a,
c are_collinear )
by DIRAF:28;
hence
contradiction
by A23, DIRAF:30;
verum
end;
c,
e1 // e4,
c
by A17, DIRAF:2;
then
c,
e1 // e2,
e5
by A44, A48, DIRAF:3;
then
p,
a // e2,
e5
by A13, A29, DIRAF:3;
then
e2,
e3 // e2,
e5
by A3, A22, ANALOAF:def 5;
then
(
Mid e2,
e3,
e5 or
Mid e2,
e5,
e3 )
by DIRAF:7;
then
(
e2,
e3,
e5 are_collinear or
e2,
e5,
e3 are_collinear )
by DIRAF:28;
then A61:
e2,
e3,
e5 are_collinear
by DIRAF:30;
Mid p,
c,
e3
by A21, DIRAF:def 3;
then A62:
Mid e3,
c,
p
by DIRAF:9;
e3,
c // c,
p
by A21, DIRAF:2;
then consider x being
Element of
OAS such that A63:
e5,
c // c,
x
and A64:
e5,
e3 // p,
x
by A34, ANALOAF:def 5;
A65:
c,
e5 // x,
c
by A63, DIRAF:2;
Mid p,
c,
e3
by A21, DIRAF:def 3;
then
Mid e3,
c,
p
by DIRAF:9;
then
e3,
c // c,
p
by DIRAF:def 3;
then
e3,
c // e3,
p
by ANALOAF:def 5;
then
e3,
p // e3,
c
by DIRAF:2;
then
not
Mid e2,
e3,
e5
by A60, A57, A42, Th17;
then
(
Mid e3,
e2,
e5 or
Mid e2,
e5,
e3 )
by A61, DIRAF:29;
then
(
e3,
e2 // e2,
e5 or
Mid e3,
e5,
e2 )
by DIRAF:9, DIRAF:def 3;
then
(
e3,
e2 // e3,
e5 or
e3,
e5 // e5,
e2 )
by ANALOAF:def 5, DIRAF:def 3;
then A66:
e3,
e5 // e3,
e2
by ANALOAF:def 5, DIRAF:2;
c,
e5 // p,
e2
by A57, DIRAF:2;
then
Mid e3,
e5,
e2
by A34, A42, A66, A62, Th15;
then
Mid e2,
e5,
e3
by DIRAF:9;
then A67:
e2,
e5 // e5,
e3
by DIRAF:def 3;
then
e2,
e5 // e2,
e3
by ANALOAF:def 5;
then
e2,
e3 // e5,
e3
by A45, A67, ANALOAF:def 5;
then
p,
a // e5,
e3
by A22, A28, DIRAF:3;
then
p,
a // p,
x
by A64, A60, DIRAF:3;
then A68:
p,
x // p,
a
by DIRAF:2;
a,
b // c,
e5
by A43, A33, A58, DIRAF:3;
then A69:
a,
b // x,
c
by A52, A65, DIRAF:3;
then
c,
x // b,
a
by DIRAF:2;
hence
ex
x being
Element of
OAS st
(
Mid p,
x,
a &
a,
b // x,
c )
by A1, A2, A11, A69, A68, Th15;
verum end;
A70:
( a = c implies ( a,b // a,c & Mid p,a,a ) )
by DIRAF:4, DIRAF:10;
A71:
( p = c implies ( a,b // c,c & Mid p,c,a ) )
by DIRAF:4, DIRAF:10;
( b = c implies ( a,b // a,c & Mid p,a,a ) )
by DIRAF:1, DIRAF:10;
hence
ex x being Element of OAS st
( Mid p,x,a & a,b // x,c )
by A8, A70, A71; verum