let
X
be
BCI-algebra
;
:: thesis:
0.
X
in
AtomSet
X
for
z
being
Element
of
X
st
z
\
(
0.
X
)
=
0.
X
holds
z
=
0.
X
by
Th2
;
then
0.
X
is
atom
;
hence
0.
X
in
AtomSet
X
;
:: thesis:
verum