let OAS be OAffinSpace; :: thesis: for a, b, c, d, x being Element of OAS st Mid a,b,d & Mid b,x,c & not a,b,c are_collinear holds
ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
let a, b, c, d, x be Element of OAS; :: thesis: ( Mid a,b,d & Mid b,x,c & not a,b,c are_collinear implies ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) )
assume that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not a,b,c are_collinear ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
A4: now :: thesis: ( b = d implies ex y being Element of OAS st
( Mid a,y,c & Mid d,x,y & Mid a,y,c & Mid y,x,d ) )
assume A5: b = d ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid d,x,y & Mid a,y,c & Mid y,x,d )
take y = c; :: thesis: ( Mid a,y,c & Mid d,x,y & Mid a,y,c & Mid y,x,d )
thus ( Mid a,y,c & Mid d,x,y ) by A2, A5, DIRAF:10; :: thesis: ( Mid a,y,c & Mid y,x,d )
thus ( Mid a,y,c & Mid y,x,d ) by A2, A5, DIRAF:9, DIRAF:10; :: thesis: verum
end;
A6: Mid d,b,a by A1, DIRAF:9;
A7: now :: thesis: ( b <> d & x <> b implies ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) )
assume that
A8: b <> d and
A9: x <> b ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
d,b // b,a by A6, DIRAF:def 3;
then consider e1 being Element of OAS such that
A10: x,b // b,e1 and
A11: x,d // a,e1 by A8, ANALOAF:def 5;
A12: Mid x,b,e1 by A10, DIRAF:def 3;
then A13: Mid e1,b,x by DIRAF:9;
then A14: Mid e1,x,c by A2, A9, DIRAF:12;
A15: c <> e1
proof
assume c = e1 ; :: thesis: contradiction
then Mid x,b,x by A2, A9, A13, DIRAF:8, DIRAF:12;
hence contradiction by A9, DIRAF:8; :: thesis: verum
end;
A16: x <> e1 by A9, A12, DIRAF:8;
A17: not c,a,e1 are_collinear
proof
x,b,e1 are_collinear by A12, DIRAF:28;
then A18: x,e1,b are_collinear by DIRAF:30;
assume c,a,e1 are_collinear ; :: thesis: contradiction
then A19: c,e1,a are_collinear by DIRAF:30;
c,x,e1 are_collinear by A14, DIRAF:9, DIRAF:28;
then A20: c,e1,x are_collinear by DIRAF:30;
A21: c,e1,c are_collinear by DIRAF:31;
c,e1,e1 are_collinear by DIRAF:31;
then c,e1,b are_collinear by A16, A20, A18, DIRAF:35;
hence contradiction by A3, A15, A19, A21, DIRAF:32; :: thesis: verum
end;
Mid c,x,e1 by A14, DIRAF:9;
then consider y being Element of OAS such that
A22: Mid c,y,a and
A23: a,e1 // y,x by A17, Th21;
a <> e1 by A17, DIRAF:31;
then x,d // y,x by A11, A23, DIRAF:3;
then d,x // x,y by DIRAF:2;
then Mid d,x,y by DIRAF:def 3;
then A24: Mid y,x,d by DIRAF:9;
Mid a,y,c by A22, DIRAF:9;
hence ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) by A24; :: thesis: verum
end;
now :: thesis: ( b <> d & x = b implies ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) )
assume that
b <> d and
A25: x = b ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
take y = a; :: thesis: ( Mid a,y,c & Mid y,x,d )
thus ( Mid a,y,c & Mid y,x,d ) by A1, A25, DIRAF:10; :: thesis: verum
end;
hence ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) by A7, A4; :: thesis: verum