\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{Idempotency\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{theorem}
 $ a \cup  a = a $.
\end{theorem}
\begin{ilfproof}{\mbox{Otter} and \mbox{Ilf}} We show directly that \ilfformula{
a \cup  a = a\mbox{.}
\label{[1,1]}
}


 Because of $ $Huntington's axiom$ $ and by $ $associativity$ $\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{1} \cup  \overline{{x}_{2}}} \cup  \overline{\overline{{x}_{1}} \cup  \overline{{x}_{2}}} \cup  {x}_{3} = {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),36]}
}

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),8]}
}


$ $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),8]}).

 Hence  by $ $Huntington's axiom$ $\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{1} \cup  \overline{{x}_{3}}} \cup  {x}_{2} \cup  \overline{\overline{{x}_{1}} \cup  \overline{{x}_{3}}} = {x}_{2} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),34]}
}

 Because of $ $commutativity$ $ and by $ $Huntington's axiom$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{\overline{{x}_{2}} \cup  {x}_{1}} \cup  \overline{\overline{{x}_{1}} \cup  \overline{{x}_{2}}} = {x}_{2}\mbox{.}
\label{[sub(1,1),25]}
}

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

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

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

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

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

 Because of $ $commutativity$ $ and by $ $Huntington's axiom$ $\ilfformula{
\forall ({x}_{1},{x}_{2})\ \overline{{x}_{1} \cup  \overline{{x}_{2}}} \cup  \overline{\overline{{x}_{2}} \cup  \overline{{x}_{1}}} = {x}_{2}\mbox{.}
\label{[sub(1,1),29]}
}

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

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

 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),9]}
}

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

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


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

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

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

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


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

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

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


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

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

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

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


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

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

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


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

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


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

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

 Therefore $\forall ({x}_{1},{x}_{2})\ {x}_{1} \cup  {x}_{1} \cup  \overline{{x}_{1}} = \overline{{x}_{2}} \cup  {x}_{2}\mbox{.} $
 Hence  by (\ref{[sub(1,1),5005]}) $\forall ({x}_{1},{x}_{2},{x}_{3})\ {x}_{1} \cup  {x}_{2} \cup  \overline{{x}_{2}} = \overline{{x}_{3}} \cup  {x}_{3}\mbox{.} $
 Hence  by (\ref{[sub(1,1),17]})\ilfformula{
\forall ({x}_{1},{x}_{2},{x}_{3})\ \overline{{x}_{1}} \cup  {x}_{1} \cup  {x}_{2} = \overline{{x}_{3}} \cup  {x}_{3}\mbox{.}
\label{[sub(1,1),5630]}
}

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


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

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


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

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

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


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),5207]}), (\ref{[sub(1,1),2085]}), (\ref{[sub(1,1),4724]}), and by $ $associativity$ $ $ $
\begin{eqnarray*}
\overline{\overline{{v}_{1}} \cup  {v}_{1}} \cup  {v}_{2} & = & {v}_{2} \cup  \overline{(\overline{\overline{{v}_{2}}} \cup  \overline{\overline{{v}_{2}}}) \cup  \overline{{v}_{2}}}\\
 & = & {v}_{2} \cup  \overline{({v}_{2} \cup  \overline{\overline{{v}_{2}}}) \cup  \overline{{v}_{2}}}\\
 & = & {v}_{2} \cup  \overline{({v}_{2} \cup  {v}_{2}) \cup  \overline{{v}_{2}}}\\
\overline{\overline{{v}_{1}} \cup  {v}_{1}} \cup  {v}_{2} & = & {v}_{2} \cup  \overline{{v}_{2} \cup  {v}_{2} \cup  \overline{{v}_{2}}}
\mbox{.}\end{eqnarray*}
$ $
This completes the proof of (\ref{[sub(1,1),5240]}).

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

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


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

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


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

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

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

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


$ $Let us consider arbitrary $ {v}_{1},{v}_{2}$.$ $ By (\ref{[sub(1,1),6276]}), (\ref{[sub(1,1),4441]}), and by (\ref{[sub(1,1),6105]}) ${v}_{2} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{1} \cup  \overline{{v}_{1}}}}} = \overline{{v}_{1} \cup  \overline{{v}_{1}}} \cup  \overline{\overline{{v}_{2}} \cup  \overline{{v}_{2}}} = \overline{\overline{{v}_{2}}}\mbox{.} $
 Hence  by (\ref{[sub(1,1),4724]}) ${v}_{2} = {v}_{2} \cup  \overline{{v}_{2} \cup  \overline{\overline{{v}_{1} \cup  \overline{{v}_{1}}}}} = {v}_{2} \cup  \overline{{v}_{2} \cup  {v}_{1} \cup  \overline{{v}_{1}}}\mbox{.} $
This completes the proof of (\ref{[sub(1,1),6319]}).

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




\end{ilfproof}

\end{document}
