let
X
be
BCI-algebra
;
:: thesis:
for
x
being
Element
of
X
holds
x
`
in
AtomSet
X
let
x
be
Element
of
X
;
:: thesis:
x
`
in
AtomSet
X
0.
X
in
AtomSet
X
by
Th23
;
hence
x
`
in
AtomSet
X
by
Th33
;
:: thesis:
verum