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