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 )

( Mid a,y,c & Mid y,x,d ) by A7, A4; :: thesis: verum

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 ) )

A6:
Mid d,b,a
by A1, DIRAF:9;( 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;( 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

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

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

( 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

A17: not c,a,e1 are_collinear

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;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

A16:
x <> e1
by A9, A12, DIRAF:8;
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;then Mid x,b,x by A2, A9, A13, DIRAF:8, DIRAF:12;

hence contradiction by A9, DIRAF:8; :: thesis: verum

A17: not c,a,e1 are_collinear

proof

Mid c,x,e1
by A14, DIRAF:9;
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;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

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

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

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

hence
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;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

( Mid a,y,c & Mid y,x,d ) by A7, A4; :: thesis: verum