let OAS be OAffinSpace; :: thesis: for a, a9, b, b9, c, c9 being Element of OAS st not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds
Mid a9,b9,c9
let a, a9, b, b9, c, c9 be Element of OAS; :: thesis: ( not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear implies Mid a9,b9,c9 )
assume that
A1: not a,b,a9 are_collinear and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: a9,b9,c9 are_collinear ; :: thesis: Mid a9,b9,c9
A6: a,b,c are_collinear by A4, DIRAF:28;
A7: b9,c9,a9 are_collinear by A5, DIRAF:30;
A8: c9,b9,a9 are_collinear by A5, DIRAF:30;
A9: a <> a9 by A1, DIRAF:31;
then A10: b,b9 '||' c,c9 by A2, A3, DIRAF:23;
A11: a <> b by A1, DIRAF:31;
then A12: a <> c by A4, DIRAF:8;

A13: now :: thesis: ( b9 <> c9 & a9 <> b9 & b <> b9 implies Mid a9,b9,c9 )

assume that
A14: b9 <> c9 and
a9 <> b9 and
A15: b <> b9 ; :: thesis: Mid a9,b9,c9
A16: not b,b9,a9 are_collinear

proof

A17: b,b9,b are_collinear by DIRAF:31;
assume A18: b,b9,a9 are_collinear ; :: thesis: contradiction
b,b9 '||' a9,a by A2, DIRAF:22;
then b,b9,a are_collinear by A15, A18, DIRAF:33;
hence contradiction by A1, A15, A18, A17, DIRAF:32; :: thesis: verum

end;

A19: now :: thesis: ( c <> c9 implies Mid a9,b9,c9 )

a,b '||' a,c by A6, DIRAF:def 5;
then c,a '||' a,b by DIRAF:22;
then consider x being Element of OAS such that
A20: c9,a '||' a,x and
A21: c9,c '||' b,x by A12, DIRAF:27;
a,c9 '||' a,x by A20, DIRAF:22;
then A22: a,c9,x are_collinear by DIRAF:def 5;
assume A23: c <> c9 ; :: thesis: Mid a9,b9,c9
A24: x <> b

proof

assume x = b ; :: thesis: contradiction
then A25: a,b,c9 are_collinear by A22, DIRAF:30;
a,b,b are_collinear by DIRAF:31;
then A26: c,c9,b are_collinear by A11, A6, A25, DIRAF:32;
a,b,a are_collinear by DIRAF:31;
then c,c9,a are_collinear by A11, A6, A25, DIRAF:32;
then c,c9 '||' a,b by A26, DIRAF:34;
then b,b9 '||' a,b by A10, A23, DIRAF:23;
then a,a9 '||' a,b by A2, A15, DIRAF:23;
then a,a9,b are_collinear by DIRAF:def 5;
hence contradiction by A1, DIRAF:30; :: thesis: verum

end;

c,c9 '||' b,x by A21, DIRAF:22;
then b,b9 '||' b,x by A10, A23, DIRAF:23;
then A27: b,b9,x are_collinear by DIRAF:def 5;
then b,x,b9 are_collinear by DIRAF:30;
then b,x '||' b,b9 by DIRAF:def 5;
then b,x '||' c,c9 by A10, A15, DIRAF:23;
then A28: x,b '||' c,c9 by DIRAF:22;
A29: x <> b9

proof

assume x = b9 ; :: thesis: contradiction
then A30: b9,c9,a are_collinear by A22, DIRAF:30;
A31: a,a9 '||' b9,b by A2, DIRAF:22;
b9,c9,b9 are_collinear by DIRAF:31;
then a,a9,b9 are_collinear by A7, A14, A30, DIRAF:32;
then a,a9,b are_collinear by A9, A31, DIRAF:33;
hence contradiction by A1, DIRAF:30; :: thesis: verum

end;

A32: not c9,b9,x are_collinear

proof

assume c9,b9,x are_collinear ; :: thesis: contradiction
then A33: b9,x,c9 are_collinear by DIRAF:30;
A34: b9,x,b9 are_collinear by DIRAF:31;
A35: c9,b9,b9 are_collinear by DIRAF:31;
b9,x,b are_collinear by A27, DIRAF:30;
then c9,b9,b are_collinear by A29, A33, A34, DIRAF:32;
hence contradiction by A8, A14, A16, A35, DIRAF:32; :: thesis: verum

end;

A36: x,b,b9 are_collinear by A27, DIRAF:30;
A37: not a,x,b are_collinear

proof

assume a,x,b are_collinear ; :: thesis: contradiction
then A38: x,b,a are_collinear by DIRAF:30;
A39: b,b9 '||' a,a9 by A2, DIRAF:22;
x,b,b are_collinear by DIRAF:31;
then b,b9,a are_collinear by A36, A24, A38, DIRAF:32;
hence contradiction by A15, A16, A39, DIRAF:33; :: thesis: verum

end;

b9,b,x are_collinear by A27, DIRAF:30;
then b9,b '||' b9,x by DIRAF:def 5;
then b,b9 '||' b9,x by DIRAF:22;
then A40: b9,x '||' a,a9 by A2, A15, DIRAF:23;
a,x,c9 are_collinear by A22, DIRAF:30;
then Mid a,x,c9 by A4, A28, A37, Th8;
then Mid c9,x,a by DIRAF:9;
then Mid c9,b9,a9 by A8, A40, A32, Th8;
hence Mid a9,b9,c9 by DIRAF:9; :: thesis: verum

end;

( c = c9 implies Mid a9,b9,c9 )

proof

A41: not c9,b9,b are_collinear

proof

A42: c9,b9,b9 are_collinear by DIRAF:31;
assume c9,b9,b are_collinear ; :: thesis: contradiction
hence contradiction by A8, A14, A16, A42, DIRAF:32; :: thesis: verum

end;

assume c = c9 ; :: thesis: Mid a9,b9,c9
then A43: Mid c9,b,a by A4, DIRAF:9;
b9,b '||' a,a9 by A2, DIRAF:22;
then Mid c9,b9,a9 by A8, A43, A41, Th8;
hence Mid a9,b9,c9 by DIRAF:9; :: thesis: verum

end;

hence Mid a9,b9,c9 by A19; :: thesis: verum

end;

( b = b9 implies Mid a9,b9,c9 )

proof

A44: a,a9 '||' c9,c by A3, DIRAF:22;
A45: b9,a9,c9 are_collinear by A5, DIRAF:30;
assume A46: b = b9 ; :: thesis: Mid a9,b9,c9
then not b9,a,a9 are_collinear by A1, DIRAF:30;
hence Mid a9,b9,c9 by A4, A46, A45, A44, Th6; :: thesis: verum

end;

hence Mid a9,b9,c9 by A13, DIRAF:10; :: thesis: verum