let
E
be
set
;
:: thesis:
for
A
being
Subset
of
(
E
^omega
)
holds
(
A
+
)
^^
A
=
A
|^..
2
let
A
be
Subset
of
(
E
^omega
)
;
:: thesis:
(
A
+
)
^^
A
=
A
|^..
2
(
A
+
)
^^
A
=
(
A
+
)
^^
(
A
|^
1
)
by
FLANG_1:25
.=
A
|^..
(
1
+
1
)
by
Th75
;
hence
(
A
+
)
^^
A
=
A
|^..
2 ;
:: thesis:
verum