let
X
be
BCI-Algebra_with_Condition(S)
;
:: thesis:
for
x
being
Element
of
X
holds
x
|^
3
=
(
x
*
x
)
*
x
let
x
be
Element
of
X
;
:: thesis:
x
|^
3
=
(
x
*
x
)
*
x
thus
x
|^
3 =
x
|^
(
2
+
1
)
.=
(
x
|^
2
)
*
x
by
Def6
.=
(
x
*
x
)
*
x
by
Th22
;
:: thesis:
verum