let OAS be OAffinSpace; :: thesis: 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; :: thesis: ex x being Element of OAS st
( a,x // b,c & a,b // x,c )
A1: now :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: contradiction
hence contradiction by A5, A42, A44, A45, DIRAF:32; :: thesis: verum
end;
A46: e5 <> e3
proof
assume e5 = e3 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
A58: a <> e2
proof
assume A59: a = e2 ; :: thesis: 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; :: thesis: verum
end;
A60: e6 <> x
proof
assume e6 = x ; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( a,b,c are_collinear implies ex x being Element of OAS st
( a,x // b,c & a,b // x,c ) )
A72: now :: thesis: ( Mid a,c,b implies ( a,a // b,c & a,b // a,c ) )
assume Mid a,c,b ; :: thesis: ( 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; :: thesis: verum
end;
A73: now :: thesis: ( Mid b,a,c implies ( a,c // b,c & a,b // c,c ) )
assume Mid b,a,c ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
hence ex x being Element of OAS st
( a,x // b,c & a,b // x,c ) by A1; :: thesis: verum