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