let
X
be
BCI-algebra
;
:: thesis:
0.
X
in
BCK-part
X
(
0.
X
)
`
=
0.
X
by
Def5
;
then
0.
X
<=
0.
X
;
hence
0.
X
in
BCK-part
X
;
:: thesis:
verum