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

( 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