1: \begin{proof}

2:   The lemma can be rigorously proved by \emph{Mathematica}. The codes

3:   are in Section~\ref{sec:computer}.

4:   % \begin{lstlisting}

5:   %   Phi[x_] := 1/x/(1/2-x); M = (Maximize[{1/Phi[x]/(1-x),

6:   %   0<=x<=1/2},

7:   %   {x}])[[1]]; F[k_] := (1-f[k])(1-y[k])/Sum[(1-f[i])(1-y[i]),

8:   %   {i,1,4}]; dMP = Phi[F[1]] F[1] ((1-F[1])/(1-y[1])/Phi[y[1]] +

9:   %   Sum[F[j]/(1-y[j])/Phi[y[j]], {j,2,4}] + 4f[1]M

10:   %   Sum[F[k]/(1-f[k]),

11:   %   {k,2,4}]); dMSy = dMP /. {f[2]->(1-f[1])/3, f[3]->(1-f[1])/3,

12:   %   f[4]->(1-f[1])/3, y[3]->y[2], y[4]->y[2]};

13:   %   Resolve[Exists[{f[1],y[1],y[2]}, dMSy>=963/1000 &&

14:   %   1/13<=f[1]<=1/2

15:   %   && 0<=y[1]<=1/2 && 0<=y[2]<=1/2]]

16:   % \end{lstlisting}

17: \end{proof}

18: