let OAS be OAffinSpace; :: thesis: for a, b, d, x, c being Element of OAS st Mid a,b,d & Mid a,x,c & not LIN a,b,c holds
ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
let a, b, d, x, c be Element of OAS; :: thesis: ( Mid a,b,d & Mid a,x,c & not LIN a,b,c implies ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) )
assume that
A1: Mid a,b,d and
A2: Mid a,x,c and
A3: not LIN a,b,c ; :: thesis: ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
A4: ( a <> b & a <> c & b <> c ) by A3, DIRAF:37;

A5: now

assume A6: ( b <> d & x <> c & a <> x ) ; :: thesis: ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d )
then consider e1 being Element of OAS such that
A7: Mid a,d,e1 and
A8: x,d // c,e1 by A2, Th27;
A9: ( Mid d,b,a & Mid e1,d,a ) by A1, A7, DIRAF:13;
A10: ( LIN d,b,a & LIN e1,d,a ) by A1, A7, DIRAF:13, DIRAF:34;
A11: e1 <> b by A6, A9, DIRAF:18;
Mid b,d,e1 by A1, A7, DIRAF:15;
then Mid e1,d,b by DIRAF:13;
then Mid e1,b,a by A9, DIRAF:16;
then e1,b // b,a by DIRAF:def 3;
then consider e2 being Element of OAS such that
A12: c,b // b,e2 and
A13: c,e1 // a,e2 by A11, ANALOAF:def 5;
A14: Mid c,b,e2 by A12, DIRAF:def 3;
then A15: LIN c,b,e2 by DIRAF:34;
A16: a <> d by A1, A6, DIRAF:12;
A17: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then ( LIN d,a,b & LIN d,a,c & LIN d,a,a ) by A10, DIRAF:36, DIRAF:37;
hence contradiction by A3, A16, DIRAF:38; :: thesis: verum

end;

A18: a <> e2

proof

assume a = e2 ; :: thesis: contradiction
then Mid c,b,a by A12, DIRAF:def 3;
hence contradiction by A3, DIRAF:13, DIRAF:34; :: thesis: verum

end;

Mid c,x,a by A2, DIRAF:13;
then consider y being Element of OAS such that
A19: Mid c,y,e2 and
A20: a,e2 // x,y by Th26;
A21: not LIN a,x,b

proof

assume LIN a,x,b ; :: thesis: contradiction
then ( LIN a,x,b & LIN a,x,c & LIN a,x,a ) by A2, DIRAF:34, DIRAF:37;
hence contradiction by A3, A6, DIRAF:38; :: thesis: verum

end;

A22: not LIN x,d,a

proof

assume LIN x,d,a ; :: thesis: contradiction
then ( LIN d,a,x & LIN d,a,b & LIN d,a,a ) by A10, DIRAF:36, DIRAF:37;
hence contradiction by A16, A21, DIRAF:38; :: thesis: verum

end;

then A23: x <> d by DIRAF:37;
A24: c <> e2 by A4, A12, ANALOAF:def 5;
x,d // a,e2 by A8, A13, A17, DIRAF:6;
then x,d // x,y by A18, A20, DIRAF:6;
then A25: ( Mid x,d,y or Mid x,y,d ) by DIRAF:11;

A26: now

assume A27: Mid x,d,y ; :: thesis: contradiction
then consider c' being Element of OAS such that
A28: Mid x,c',a and
A29: Mid c',b,y by A9, A22, Th35;
A30: b <> y

proof

assume b = y ; :: thesis: contradiction
then LIN x,d,b by A27, DIRAF:34;
then ( LIN d,b,x & LIN a,x,c ) by A2, DIRAF:34, DIRAF:36;
then ( LIN d,b,c & LIN d,b,b ) by A6, A10, DIRAF:37, DIRAF:41;
hence contradiction by A3, A6, A10, DIRAF:38; :: thesis: verum

end;

( LIN a,x,c & LIN x,c',a ) by A2, A28, DIRAF:34;
then ( LIN x,a,c & LIN x,a,c' & LIN x,a,a ) by DIRAF:36, DIRAF:37;
then A31: LIN c,c',a by A6, DIRAF:38;
( LIN c,y,e2 & LIN c,b,e2 ) by A14, A19, DIRAF:34;
then ( LIN c,e2,y & LIN c,e2,b & LIN c,e2,c ) by DIRAF:36, DIRAF:37;
then ( LIN b,y,c & LIN c',b,y ) by A24, A29, DIRAF:34, DIRAF:38;
then ( LIN b,y,c & LIN b,y,c' & LIN b,y,b ) by DIRAF:36, DIRAF:37;
then ( LIN c,c',b & LIN c,c',c ) by A30, DIRAF:38;
then ( Mid x,c,a & Mid c,x,a ) by A2, A3, A28, A31, DIRAF:13, DIRAF:38;
hence contradiction by A6, DIRAF:18; :: thesis: verum

end;

then A32: Mid d,y,x by A25, DIRAF:13;
A33: ( Mid c,b,y or Mid c,y,b ) by A14, A19, DIRAF:21;

now

assume A34: not Mid c,y,b ; :: thesis: contradiction
then A35: y <> b by DIRAF:14;
Mid b,y,e2 by A19, A33, A34, DIRAF:15;
then consider z being Element of OAS such that
A36: ( Mid b,d,z & y,d // e2,z ) by A35, Th27;
A37: y <> d

proof

assume y = d ; :: thesis: contradiction
then LIN c,d,e2 by A19, DIRAF:34;
then A38: ( LIN c,e2,d & LIN c,e2,b ) by A15, DIRAF:36;
then ( LIN c,e2,a & LIN c,e2,c ) by A6, A10, DIRAF:37, DIRAF:41;
hence contradiction by A3, A24, A38, DIRAF:38; :: thesis: verum

end;

d,y // y,x by A32, DIRAF:def 3;
then d,y // d,x by ANALOAF:def 5;
then y,d // x,d by DIRAF:5;
then y,d // c,e1 by A8, A23, DIRAF:6;
then c,e1 // e2,z by A36, A37, ANALOAF:def 5;
then a,e2 // e2,z by A13, A17, ANALOAF:def 5;
then Mid a,e2,z by DIRAF:def 3;
then LIN a,e2,z by DIRAF:34;
then A39: LIN a,z,e2 by DIRAF:36;
A40: b <> e2

proof

assume b = e2 ; :: thesis: contradiction
then ( c,e1 // a,b & c,e1 // x,d ) by A8, A13, DIRAF:5;
then ( a,b // x,d & a,b // b,d ) by A1, A17, ANALOAF:def 5, DIRAF:def 3;
then x,d // b,d by A4, ANALOAF:def 5;
then d,x // d,b by DIRAF:5;
then ( Mid d,x,b or Mid d,b,x ) by DIRAF:11;
then ( LIN d,x,b or LIN d,b,x ) by DIRAF:34;
then ( LIN d,b,x & LIN d,b,b ) by DIRAF:36, DIRAF:37;
then ( LIN a,x,b & LIN a,x,c & LIN a,x,a ) by A2, A6, A10, DIRAF:34, DIRAF:38;
hence contradiction by A3, A6, DIRAF:38; :: thesis: verum

end;

( LIN b,d,z & LIN b,d,a & LIN b,d,b ) by A10, A36, DIRAF:34, DIRAF:36, DIRAF:37;
then A41: ( LIN a,z,b & LIN a,z,a ) by A6, DIRAF:38;

now

assume a = z ; :: thesis: contradiction
then ( Mid b,d,a & Mid d,b,a ) by A1, A36, DIRAF:13;
hence contradiction by A6, DIRAF:18; :: thesis: verum

end;

then A42: ( LIN a,e2,b & LIN a,e2,e2 & LIN b,e2,c ) by A15, A39, A41, DIRAF:36, DIRAF:38;
then ( LIN a,e2,c & LIN a,e2,a ) by A40, DIRAF:37, DIRAF:41;
hence contradiction by A3, A18, A42, DIRAF:38; :: thesis: verum

end;

then Mid b,y,c by DIRAF:13;
hence ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) by A25, A26; :: thesis: verum

end;

A43: ( b = d implies ( Mid b,d,c & Mid x,d,d ) ) by DIRAF:14;
A44: ( x = c implies ( Mid b,c,c & Mid x,c,d ) ) by DIRAF:14;
( a = x implies ( Mid b,b,c & Mid x,b,d ) ) by A1, DIRAF:14;
hence ex y being Element of OAS st
( Mid b,y,c & Mid x,y,d ) by A5, A43, A44; :: thesis: verum