let
E
be
set
;
:: thesis:
for
A
being
Subset
of
(
E
^omega
)
holds
(
A
*
)
^^
(
A
+
)
=
(
A
+
)
^^
(
A
*
)
let
A
be
Subset
of
(
E
^omega
)
;
:: thesis:
(
A
*
)
^^
(
A
+
)
=
(
A
+
)
^^
(
A
*
)
thus
(
A
*
)
^^
(
A
+
)
=
(
A
*
)
^^
(
A
|^..
1
)
by
Th50
.=
(
A
|^..
1
)
^^
(
A
*
)
by
Th32
.=
(
A
+
)
^^
(
A
*
)
by
Th50
;
:: thesis:
verum