let E be set ; :: thesis: for A being Subset of (E ^omega) holds
( A + = A * iff <%> E in A )
let A be Subset of (E ^omega); :: thesis: ( A + = A * iff <%> E in A )
thus ( A + = A * implies <%> E in A ) :: thesis: ( <%> E in A implies A + = A * )

proof

assume A + = A * ; :: thesis: <%> E in A
then <%> E in A + by FLANG_1:48;
hence <%> E in A by Th56; :: thesis: verum

end;

assume <%> E in A ; :: thesis: A + = A *
then A * = (A *) ^^ A by FLANG_1:54;
hence A + = A * by Th52; :: thesis: verum