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