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 +

A + c= (A +) + by Th59;

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

let A be Subset of (E ^omega); :: thesis: (A +) + = A +

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

x in A +

then A4:
(A +) + c= A +
;x in A +

let x be object ; :: thesis: ( x in (A +) + implies b_{1} in A + )

assume A1: x in (A +) + ; :: thesis: b_{1} in A +

end;assume A1: x in (A +) + ; :: thesis: b

A + c= (A +) + by Th59;

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