\documentstyle{article}

% ILF_STYLE 1.2 (01/21/97)
  \newlength{\ilfformulalength}\setlength{\ilfformulalength}{\textwidth}
  \addtolength{\ilfformulalength}{-7em}
  \ifx\mathindent\undefined
    \newcommand{\ilftformel}[1]{\begin{equation}%
\parbox{\ilfformulalength}{\centering #1}\end{equation}}
  \else
    \addtolength{\ilfformulalength}{-\mathindent}
    \newcommand{\ilftformel}[1]{\begin{equation}%
\parbox{\ilfformulalength}{#1}\end{equation}}
\fi
  \newcommand{\ilfformula}[1]{\ilftformel{$ #1 $}}
  \newenvironment{ilfproof}[1]{%
Proof\/\footnote{#1}.}{\begin{quote}\raggedleft q.e.d.\end{quote}}
  \newenvironment{ilf_cases}{%
\renewcommand{\labelenumi}{Case \arabic{enumi}.}\begin{enumerate}}%
{\end{enumerate}}
  \newcommand{\ilfUpCase}[1]{\ifmmode#1\else\uppercase{#1}\fi}
  \newcounter{ilflistdepth}\setcounter{ilflistdepth}{0}
  \newcounter{ilflistolddepth}
  \newcounter{ilflistmaxdepth}\setcounter{ilflistmaxdepth}{0}
  \newlength{\ilflistmargin}\settowidth{\ilflistmargin}{1.\ }
  \newcommand\ilflistempty{}
  \newcommand\ilflistconstlabel{}
  \def\ilflistlabeli{}
  \def\ilflistsetlabel#1#2{\ifnum#2=0\else
\ilflistsetlabelA{\romannumeral#1}{\romannumeral#2}\fi}
  \def\ilflistsetlabelA#1#2{\expandafter\xdef\csname ilflistlabel#1\endcsname{%
\csname ilflistlabel#2\endcsname\arabic{ilflist#2}.\ }}
  \def\ilflistlabel#1{\ilflistconstlabel%
\csname ilflistlabel#1\endcsname\arabic{ilflist#1}.\ }
\expandafter\def\csname p@ilflisti\endcsname{}
  \def\ilflistsetpa#1#2{\ifnum#2=0\else
\ilflistsetpaA{\romannumeral#1}{\romannumeral#2}\fi}
  \def\ilflistsetpaA#1#2{\expandafter\xdef\csname p@ilflist#1\endcsname{%
\csname p@ilflist#2\endcsname\arabic{ilflist#2}.}}
  \newenvironment{ilflist}[1]{\par\vspace{\topsep}\parskip\parsep%
\advance\leftskip by \ilflistmargin%
\ifnum\theilflistdepth=0\advance\leftskip by \ilflistmargin\fi%
\renewcommand\ilflistconstlabel{#1}
\ifx\ilflistconstlabel\ilflistempty\else\renewcommand\ilflistconstlabel{#1\ }\fi
\setcounter{ilflistolddepth}{\theilflistdepth}
\addtocounter{ilflistdepth}{1}%
\ifnum\theilflistdepth >\theilflistmaxdepth%
\newcounter{ilflist\romannumeral\theilflistdepth}%
\setcounter{ilflistmaxdepth}{\theilflistdepth}\fi%
\setcounter{ilflist\romannumeral\theilflistdepth}{0}%
\ilflistsetpa{\theilflistdepth}{\theilflistolddepth}%
\ilflistsetlabel{\theilflistdepth}{\theilflistolddepth}}%
{\par\vspace{\topsep}%
\addtocounter{ilflistdepth}{-1}\advance\leftskip by -\ilflistmargin%
\ifnum\theilflistdepth=0\advance\leftskip by -\ilflistmargin\fi}
  \newcommand{\ilfitem}{\par\vspace{\itemsep}%
\hspace*{-\ilflistmargin}\hspace*{-\parindent}%
\refstepcounter{ilflist\romannumeral\theilflistdepth}%
\ilflistlabel{\romannumeral\theilflistdepth}\ignorespaces}
  \newtheorem{axiom}{Axiom}[section]
  \newtheorem{sysinfo}{System Information}
  \newtheorem{conjecture}{Conjecture}[section]
  \newtheorem{theorem}{Theorem}[section]
  \newtheorem{lemma}{Lemma}[section]
% END ILF_STYLE

\begin{document}

\title{Distributivity\thanks{This manuscript was generated by ILF. The development of ILF was supported by the Deutsche Forschungsgemeinschaft. For information on ILF contact \mbox{gehne@mathematik.hu-berlin.de}.}}

\author{Nelson}

\maketitle
\sloppy



\begin{axiom}[{$ $Commutativity$ $}]
 $ \forall ({x}_{1},{x}_{2})\ {x}_{2} \cup  {x}_{1} = {x}_{1} \cup  {x}_{2}\mbox{.} $
\end{axiom}
\begin{axiom}[{$ $Associativity$ $}]
 $ \forall ({x}_{1},{x}_{2},{x}_{3})\ ({x}_{1} \cup  {x}_{2}) \cup  {x}_{3} = {x}_{1} \cup  {x}_{2} \cup  {x}_{3}\mbox{.} $
\end{axiom}
\begin{axiom}[{$ $Huntington's axiom$ $}]
 $ \forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  \overline{{x}_{2}}} \cup  \overline{\overline{{x}_{1}} \cup  \overline{{x}_{2}}} = {x}_{2}\mbox{.} $
\end{axiom}
\begin{axiom}[{$ $Idempotency$ $}]
 $ \forall\ {x}_{1}\ {x}_{1} \cup  {x}_{1} = {x}_{1}\mbox{.} $
\end{axiom}
\begin{axiom}[{$ $Involution$ $}]
 $ \forall\ {x}_{1}\ \overline{\overline{{x}_{1}}} = {x}_{1}\mbox{.} $
\end{axiom}


\begin{theorem}
 $ \overline{\overline{a} \cup  \overline{b \cup  c}} = \overline{\overline{a} \cup  \overline{b}} \cup  \overline{\overline{a} \cup  \overline{c}} $.
\end{theorem}
\begin{ilfproof}{\mbox{Otter} and \mbox{Ilf}} 

We show indirectly that \ilfformula{
\overline{\overline{a} \cup  \overline{b \cup  c}} = \overline{\overline{a} \cup  \overline{b}} \cup  \overline{\overline{a} \cup  \overline{c}}\mbox{.}
\label{[1,1]}
}


Let us assume that \ilfformula{
\neg\  \overline{\overline{a} \cup  \overline{b \cup  c}} = \overline{\overline{a} \cup  \overline{b}} \cup  \overline{\overline{a} \cup  \overline{c}}\mbox{.}
\label{[sub(1,1),ax(7)]}
}

 Hence  by $ $commutativity$ $\ilfformula{
\neg\  \overline{\overline{a} \cup  \overline{c \cup  b}} = \overline{\overline{a} \cup  \overline{b}} \cup  \overline{\overline{a} \cup  \overline{c}}\mbox{.}
\label{[sub(1,1),13]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  {x}_{2}} \cup  \overline{\overline{{x}_{1}} \cup  {x}_{2}} = \overline{{x}_{2}}\mbox{.}
\label{[sub(1,1),22]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ Because of $ $involution$ $ and by $ $Huntington's axiom$ $ $\overline{{v}_{1}} = \overline{{v}_{2} \cup  {v}_{1}} \cup  \overline{\overline{{v}_{2}} \cup  \overline{\overline{{v}_{1}}}} = \overline{{v}_{2} \cup  {v}_{1}} \cup  \overline{\overline{{v}_{2}} \cup  {v}_{1}}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),22]}).

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  {x}_{2} \cup  \overline{\overline{{x}_{1}} \cup  {x}_{2}}} \cup  {x}_{2} = \overline{{x}_{1}} \cup  {x}_{2}\mbox{.}
\label{[sub(1,1),161]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),22]}) and by $ $associativity$ $ $\overline{\overline{\overline{{v}_{1}} \cup  {v}_{2}}} = \overline{({v}_{1} \cup  {v}_{2}) \cup  \overline{\overline{{v}_{1}} \cup  {v}_{2}}} \cup  \overline{\overline{{v}_{2}}} = \overline{{v}_{1} \cup  {v}_{2} \cup  \overline{\overline{{v}_{1}} \cup  {v}_{2}}} \cup  \overline{\overline{{v}_{2}}}\mbox{.} $
 Hence  by $ $involution$ $ $\overline{{v}_{1} \cup  {v}_{2} \cup  \overline{\overline{{v}_{1}} \cup  {v}_{2}}} \cup  {v}_{2} = \overline{\overline{\overline{{v}_{1}} \cup  {v}_{2}}} = \overline{{v}_{1}} \cup  {v}_{2}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),161]}).

 Because of $ $commutativity$ $ and by $ $associativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{3} \cup  {x}_{1} \cup  {x}_{2} = {x}_{1} \cup  {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),19]}
}

 Because of $ $idempotency$ $ and by $ $associativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ {x}_{1} \cup  {x}_{1} \cup  {x}_{2} = {x}_{1} \cup  {x}_{2}\mbox{.}
\label{[sub(1,1),14]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  {x}_{2}} \cup  \overline{{x}_{2}} = \overline{{x}_{2}}\mbox{.}
\label{[sub(1,1),180]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),22]}) and by (\ref{[sub(1,1),14]}) $\overline{{v}_{1} \cup  {v}_{2}} \cup  \overline{{v}_{2}} = \overline{{v}_{1} \cup  {v}_{2}} \cup  \overline{\overline{{v}_{1}} \cup  {v}_{2}} = \overline{{v}_{2}}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),180]}).

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  \overline{{x}_{2}}} \cup  {x}_{2} = {x}_{2}\mbox{.}
\label{[sub(1,1),196]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),180]}) and by $ $involution$ $ $\overline{{v}_{2} \cup  \overline{{v}_{1}}} \cup  {v}_{1} = \overline{\overline{{v}_{1}}} = {v}_{1}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),196]}).

 Hence  by $ $commutativity$ $ $\forall ({x}_{1},{x}_{2})\ \overline{\overline{{x}_{2}} \cup  {x}_{1}} \cup  {x}_{2} = {x}_{2}\mbox{.} $
 Hence  by (\ref{[sub(1,1),19]})\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{3} \cup  {x}_{2} \cup  \overline{\overline{{x}_{3}} \cup  {x}_{1}} = {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),243]}
}

 Hence  by (\ref{[sub(1,1),161]})\ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{2} \cup  {x}_{1}} \cup  {x}_{2} = \overline{{x}_{1}} \cup  {x}_{2}\mbox{.}
\label{[sub(1,1),252]}
}

 By (\ref{[sub(1,1),14]}) and by $ $commutativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ {x}_{1} \cup  {x}_{2} \cup  {x}_{1} = {x}_{1} \cup  {x}_{2}\mbox{.}
\label{[sub(1,1),41]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  {x}_{2}} \cup  {x}_{2} = \overline{{x}_{1}} \cup  {x}_{2}\mbox{.}
\label{[sub(1,1),476]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),41]}) and by (\ref{[sub(1,1),252]}) $\overline{{v}_{1} \cup  {v}_{2}} \cup  {v}_{2} = \overline{{v}_{2} \cup  {v}_{1}} \cup  {v}_{2} = \overline{{v}_{1}} \cup  {v}_{2}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),476]}).

 By (\ref{[sub(1,1),196]}) and by (\ref{[sub(1,1),19]})\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{3} \cup  {x}_{2} \cup  \overline{{x}_{1} \cup  \overline{{x}_{3}}} = {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),223]}
}

 By (\ref{[sub(1,1),22]}) and by $ $commutativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{2} \cup  {x}_{1}} \cup  \overline{\overline{{x}_{1}} \cup  {x}_{2}} = \overline{{x}_{2}}\mbox{.}
\label{[sub(1,1),155]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{2} \cup  \overline{{x}_{1} \cup  {x}_{3}}} = \overline{{x}_{2} \cup  \overline{{x}_{1}} \cup  {x}_{3}} \cup  \overline{{x}_{2} \cup  \overline{{x}_{3}}}\mbox{.}
\label{[sub(1,1),1432]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2},{v}_{3}$.$ $ By (\ref{[sub(1,1),223]}), (\ref{[sub(1,1),155]}), by $ $involution$ $, and by $ $associativity$ $ $ $
\begin{eqnarray*}
\overline{{v}_{1} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{3}}}}} & = & \overline{({v}_{1} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{3}}}}) \cup  {v}_{3}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{3}}}\\
 & = & \overline{({v}_{1} \cup  \overline{{v}_{2} \cup  {v}_{3}}) \cup  {v}_{3}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{3}}}\\
\overline{{v}_{1} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{3}}}}} & = & \overline{{v}_{1} \cup  \overline{{v}_{2} \cup  {v}_{3}} \cup  {v}_{3}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{3}}}
\mbox{.}\end{eqnarray*}
$ $
 Hence  by (\ref{[sub(1,1),476]}) and by $ $involution$ $ $\overline{{v}_{1} \cup  \overline{{v}_{2}} \cup  {v}_{3}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{3}}} = \overline{{v}_{1} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{3}}}}} = \overline{{v}_{1} \cup  \overline{{v}_{2} \cup  {v}_{3}}}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),1432]}).

 Hence  by (\ref{[sub(1,1),13]})\ilfformula{
\neg\  \overline{\overline{a} \cup  \overline{c} \cup  b} \cup  \overline{\overline{a} \cup  \overline{b}} = \overline{\overline{a} \cup  \overline{b}} \cup  \overline{\overline{a} \cup  \overline{c}}\mbox{.}
\label{[sub(1,1),1452]}
}

 By (\ref{[sub(1,1),180]}) and by $ $commutativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{2}} \cup  \overline{{x}_{1} \cup  {x}_{2}} = \overline{{x}_{2}}\mbox{.}
\label{[sub(1,1),198]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{2} \cup  {x}_{1} \cup  {x}_{3}} \cup  \overline{{x}_{2} \cup  \overline{{x}_{3}}} \cup  \overline{{x}_{2} \cup  {x}_{1}} = \overline{{x}_{2} \cup  {x}_{1} \cup  {x}_{3}} \cup  \overline{{x}_{2} \cup  \overline{{x}_{3}}}\mbox{.}
\label{[sub(1,1),1512]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2},{v}_{3}$.$ $ By (\ref{[sub(1,1),243]}), (\ref{[sub(1,1),198]}), (\ref{[sub(1,1),1432]}), and by $ $involution$ $ $ $
\begin{eqnarray*}
\overline{{v}_{1} \cup  \overline{\overline{{v}_{3}} \cup  {v}_{2}}} & = & \overline{{v}_{1} \cup  \overline{\overline{{v}_{3}} \cup  {v}_{2}}} \cup  \overline{{v}_{1} \cup  {v}_{3}}\\
 & = & (\overline{{v}_{1} \cup  \overline{\overline{{v}_{3}}} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}}) \cup  \overline{{v}_{1} \cup  {v}_{3}}\\
\overline{{v}_{1} \cup  \overline{\overline{{v}_{3}} \cup  {v}_{2}}} & = & (\overline{{v}_{1} \cup  {v}_{3} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}}) \cup  \overline{{v}_{1} \cup  {v}_{3}}
\mbox{.}\end{eqnarray*}
$ $
 Hence  by $ $associativity$ $,  (\ref{[sub(1,1),1432]}), and by $ $involution$ $ $ $
\begin{eqnarray*}
\overline{{v}_{1} \cup  {v}_{3} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}} \cup  \overline{{v}_{1} \cup  {v}_{3}} & = & \overline{{v}_{1} \cup  \overline{\overline{{v}_{3}} \cup  {v}_{2}}}\\
 & = & \overline{{v}_{1} \cup  \overline{\overline{{v}_{3}}} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}}\\
\overline{{v}_{1} \cup  {v}_{3} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}} \cup  \overline{{v}_{1} \cup  {v}_{3}} & = & \overline{{v}_{1} \cup  {v}_{3} \cup  {v}_{2}} \cup  \overline{{v}_{1} \cup  \overline{{v}_{2}}}
\mbox{.}\end{eqnarray*}
$ $
This completes the proof of (\ref{[sub(1,1),1512]}).

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{1} \cup  {x}_{2} \cup  {x}_{1} \cup  {x}_{3} = {x}_{1} \cup  {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),61]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2},{v}_{3}$.$ $ By (\ref{[sub(1,1),41]}) and by $ $associativity$ $ $({v}_{2} \cup  {v}_{1}) \cup  {v}_{3} = {v}_{2} \cup  ({v}_{1} \cup  {v}_{2}) \cup  {v}_{3}\mbox{.} $
 Hence  by $ $associativity$ $ ${v}_{2} \cup  {v}_{1} \cup  {v}_{3} = {v}_{2} \cup  ({v}_{1} \cup  {v}_{2}) \cup  {v}_{3} = {v}_{2} \cup  {v}_{1} \cup  {v}_{2} \cup  {v}_{3}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),61]}).

 By (\ref{[sub(1,1),19]}) and by (\ref{[sub(1,1),22]})\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{2} \cup  {x}_{3} \cup  {x}_{1}} \cup  \overline{\overline{{x}_{1}} \cup  {x}_{2} \cup  {x}_{3}} = \overline{{x}_{2} \cup  {x}_{3}}\mbox{.}
\label{[sub(1,1),147]}
}

 Therefore\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3},{x}_{4})\ \overline{{x}_{3} \cup  {x}_{4} \cup  {x}_{1}} \cup  {x}_{2} \cup  \overline{\overline{{x}_{1}} \cup  {x}_{3} \cup  {x}_{4}} = \overline{{x}_{3} \cup  {x}_{4} \cup  {x}_{1}} \cup  {x}_{2} \cup  \overline{{x}_{3} \cup  {x}_{4}}\mbox{.}
\label{[sub(1,1),3353]}
}

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{2} \cup  {x}_{1} \cup  {x}_{3} = {x}_{1} \cup  {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),16]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2},{v}_{3}$.$ $ Because of $ $commutativity$ $ and by $ $associativity$ $ ${v}_{1} \cup  {v}_{2} \cup  {v}_{3} = ({v}_{2} \cup  {v}_{1}) \cup  {v}_{3} = {v}_{2} \cup  {v}_{1} \cup  {v}_{3}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),16]}).

We show directly that \ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3},{x}_{4})\ \overline{{x}_{3} \cup  {x}_{4} \cup  {x}_{1}} \cup  {x}_{2} \cup  \overline{{x}_{3} \cup  {x}_{4}} = {x}_{2} \cup  \overline{{x}_{3} \cup  {x}_{4}}\mbox{.}
\label{[sub(1,1),3362]}
}


$ $Let us consider arbitrary $ {v}_{1},{v}_{2},{v}_{3},{v}_{4}$.$ $ By (\ref{[sub(1,1),147]}), (\ref{[sub(1,1),16]}), and by (\ref{[sub(1,1),3353]}) ${v}_{4} \cup  \overline{{v}_{1} \cup  {v}_{2}} = \overline{{v}_{1} \cup  {v}_{2} \cup  {v}_{3}} \cup  {v}_{4} \cup  \overline{\overline{{v}_{3}} \cup  {v}_{1} \cup  {v}_{2}} = \overline{{v}_{1} \cup  {v}_{2} \cup  {v}_{3}} \cup  {v}_{4} \cup  \overline{{v}_{1} \cup  {v}_{2}}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),3362]}).

 Hence  by (\ref{[sub(1,1),1512]}) $\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{2} \cup  \overline{{x}_{3}}} \cup  \overline{{x}_{2} \cup  {x}_{1}} = \overline{{x}_{2} \cup  {x}_{1} \cup  {x}_{3}} \cup  \overline{{x}_{2} \cup  \overline{{x}_{3}}}\mbox{.} $
This contradicts (\ref{[sub(1,1),1452]}).
Thus we have completed the proof of (\ref{[1,1]}).




\end{ilfproof}

\end{document}
