let
X
be
set
;
:: thesis:
for
x
being
Element
of
(
bspace
X
)
holds
(
1_
Z_2
)
*
x
=
x
let
x
be
Element
of
(
bspace
X
)
;
:: thesis:
(
1_
Z_2
)
*
x
=
x
reconsider
c
=
x
as
Subset
of
X
;
(
1_
Z_2
)
*
x
=
(
1_
Z_2
)
\*\
c
by
Def6
.=
c
by
Def4
;
hence
(
1_
Z_2
)
*
x
=
x
;
:: thesis:
verum