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