let
X
be
BCI-algebra
;
:: thesis:
{
(
0.
X
)
}
is
closed
Ideal
of
X
set
X1
=
{
(
0.
X
)
}
;
reconsider
X1
=
{
(
0.
X
)
}
as
Ideal
of
X
by
Lm3
;
for
x
being
Element
of
X1
holds
x
`
in
X1
by
Lm4
;
hence
{
(
0.
X
)
}
is
closed
Ideal
of
X
by
Def19
;
:: thesis:
verum