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 +

now :: thesis: for x being object st x in (A +) + holds
x in A +

let x be object ; :: thesis: ( x in (A +) + implies b₁ in A + )
assume A1: 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 A1, Th56; :: thesis: verum

end;

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

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

end;

end;

end;

then A4: (A +) + c= A + ;
A + c= (A +) + by Th59;
hence (A +) + = A + by A4, XBOOLE_0:def 10; :: thesis: verum