  A Hilbert-type axiomatic rejection $\mathbf{HAR}$ for the propositional
fragment $\mathbf{L_1}$ of Le\'{s}niewski's ontology is proposed. Also a
Gentzen-type axiomatic rejection $\mathbf{GAR}$ of $\mathbf{L_1}$ is proposed.
Models for $\mathbf{L_1}$ are introduced. By axiomatic rejection, Ishimoto's
embedding theorem will be proved. One of our main theorems is:
  \noindent \textsc{Theorem} \rm (Main Theorem) \it
  $\vdash_T A \enspace \Longleftrightarrow \enspace \vdash_H \enspace A$
  $\enspace \enspace \enspace \enspace \enspace \enspace \Longleftrightarrow
\enspace TA \enspace \mbox{is valid in first-order predicate logic with
equality}$
  $\enspace \enspace \enspace \enspace \enspace \enspace \Longleftrightarrow
\enspace not \dashv_H A.$
  \noindent where $\vdash_T A$ means that $A$ is provable in the tableau method
of $\mathbf{L_1}$, while $\vdash_H A$ means that $A$ is provable in the
Hilbert-type $\mathbf{L_1}$. \rm \smallskip
  In the last section, as the chracterization theorem, we shall show the
theorem which contains six equivalent statements with the cut elimination
theorem etc.
