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 that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not LIN a,b,c ; :: thesis: ex y being Element of OAS st
( Mid a,y,c & Mid y,x,d )

A4: now

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

end;

A6: Mid d,b,a by A1, DIRAF:13;

A7: now

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:13;
then A14: Mid e1,x,c by A2, A9, DIRAF:16;
A15: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then Mid x,b,x by A2, A9, A13, DIRAF:12, DIRAF:16;
hence contradiction by A9, DIRAF:12; :: thesis: verum

end;

A16: x <> e1 by A9, A12, DIRAF:12;
A17: not LIN c,a,e1

proof

LIN x,b,e1 by A12, DIRAF:34;
then A18: LIN x,e1,b by DIRAF:36;
assume LIN c,a,e1 ; :: thesis: contradiction
then A19: LIN c,e1,a by DIRAF:36;
LIN c,x,e1 by A14, DIRAF:13, DIRAF:34;
then A20: LIN c,e1,x by DIRAF:36;
A21: LIN c,e1,c by DIRAF:37;
LIN c,e1,e1 by DIRAF:37;
then LIN c,e1,b by A16, A20, A18, DIRAF:41;
hence contradiction by A3, A15, A19, A21, DIRAF:38; :: thesis: verum

end;

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

end;

now

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:14; :: thesis: verum

end;

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