let
E
,
x
be
set
;
:: thesis:
for
A
being
Subset
of
(
E
^omega
)
holds
(
<%
x
%>
in
A
+
iff
<%
x
%>
in
A
)
let
A
be
Subset
of
(
E
^omega
)
;
:: thesis:
(
<%
x
%>
in
A
+
iff
<%
x
%>
in
A
)
A
+
=
A
|^..
1
by
Th50
;
hence
(
<%
x
%>
in
A
+
iff
<%
x
%>
in
A
)
by
Th46
;
:: thesis:
verum