let OAS be OAffinSpace; :: thesis: for a, b, d, x, c being Element of OAS st Mid a,b,d & Mid b,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
let a, b, d, x, c be Element of OAS; :: thesis: ( Mid a,b,d & Mid b,x,c & not LIN a,b,c implies ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) )
assume A1: ( Mid a,b,d & Mid b,x,c & not LIN a,b,c ) ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
then A2: ( Mid d,b,a & Mid c,x,b ) by DIRAF:13;

A3: now

assume A4: ( b <> d & x <> b ) ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )
d,b // b,a by A2, DIRAF:def 3;
then consider e1 being Element of OAS such that
A5: ( x,b // b,e1 & x,d // a,e1 ) by A4, ANALOAF:def 5;
A6: Mid x,b,e1 by A5, DIRAF:def 3;
then A7: Mid e1,b,x by DIRAF:13;
then A8: Mid e1,x,c by A1, A4, DIRAF:16;
then A9: Mid c,x,e1 by DIRAF:13;
A10: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then Mid x,b,x by A1, A4, A7, DIRAF:12, DIRAF:16;
hence contradiction by A4, DIRAF:12; :: thesis: verum

end;

A11: x <> e1 by A4, A6, DIRAF:12;
A12: not LIN c,a,e1

proof

assume LIN c,a,e1 ; :: thesis: contradiction
then A13: LIN c,e1,a by DIRAF:36;
LIN c,x,e1 by A8, DIRAF:13, DIRAF:34;
then ( LIN c,e1,x & LIN x,b,e1 ) by A6, DIRAF:34, DIRAF:36;
then ( LIN c,e1,x & LIN c,e1,e1 & LIN x,e1,b ) by DIRAF:36, DIRAF:37;
then ( LIN c,e1,b & LIN c,e1,c ) by A11, DIRAF:37, DIRAF:41;
hence contradiction by A1, A10, A13, DIRAF:38; :: thesis: verum

end;

then consider y being Element of OAS such that
A14: ( Mid c,y,a & a,e1 // y,x ) by A9, Th28;
a <> e1 by A12, DIRAF:37;
then x,d // y,x by A5, A14, DIRAF:6;
then d,x // x,y by DIRAF:5;
then Mid d,x,y by DIRAF:def 3;
then ( Mid a,y,c & Mid y,x,d ) by A14, DIRAF:13;
hence ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) ; :: thesis: verum

end;

A15: now

assume A16: ( b <> d & 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, A16, DIRAF:14; :: thesis: verum

end;

now

assume A17: 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 A1, A17, DIRAF:14; :: thesis: ( Mid a,y,c & Mid y,x,d )
thus ( Mid a,y,c & Mid y,x,d ) by A1, A17, DIRAF:13, DIRAF:14; :: thesis: verum

end;

hence ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d ) by A3, A15; :: thesis: verum