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 ) by FLANG_1:48, Th56; :: thesis: ( <%> E in A implies A + = A * )
assume <%> E in A ; :: thesis: A + = A *
then A * = (A *) ^^ A by FLANG_1:54;
hence A + = A * by Th52; :: thesis: verum