let E be set ; :: thesis: for A being Subset of (E ^omega ) holds (A + ) + = A +
let A be Subset of (E ^omega ); :: thesis: (A + ) + = A +
A1: A + c= (A + ) + by Th59;
(A + ) + c= A +

proof

now

let x be set ; :: thesis: ( x in (A + ) + implies b₁ in A + )
assume A2: x in (A + ) + ; :: thesis: b₁ in A +

per cases ( x = <%> E or x <> <%> E ) ;

suppose x = <%> E ; :: thesis: b₁ in A +

hence x in A + by A2, Th56; :: thesis: verum

end;

suppose x <> <%> E ; :: thesis: b₁ in A +

then A3: not x in {(<%> E)} by TARSKI:def 1;
(A + ) + c= A * by Th55, Th61;
then x in A * by A2;
then x in (A + ) \/ {(<%> E)} by Th53;
hence x in A + by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence (A + ) + c= A + by TARSKI:def 3; :: thesis: verum

end;

hence (A + ) + = A + by A1, XBOOLE_0:def 10; :: thesis: verum