let E be set ; :: thesis: for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ A) *
let A, B be Subset of (E ^omega); :: thesis: ( A c= B * implies B * = (B \/ A) * )
defpred S₁[ Nat] means (B \/ A) |^ $1 c= B * ;
assume A1: A c= B * ; :: thesis: B * = (B \/ A) *

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
B c= B * by Th43;
then A4: B \/ A c= B * by A1, XBOOLE_1:8;
(B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by Th23;
hence S₁[n + 1] by A3, A4, Th46; :: thesis: verum

end;

( (B \/ A) |^ 0 = {(<%> E)} & <%> E in B * ) by Th24, Th48;
then A5: S₁[ 0 ] by ZFMISC_1:31;
A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A2);
A7: (B \/ A) * c= B *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B \/ A) * or x in B * )
assume x in (B \/ A) * ; :: thesis: x in B *
then consider n being Nat such that
A8: x in (B \/ A) |^ n by Th41;
(B \/ A) |^ n c= B * by A6;
hence x in B * by A8; :: thesis: verum

end;

B * c= (B \/ A) * by Th61, XBOOLE_1:7;
hence B * = (B \/ A) * by A7, XBOOLE_0:def 10; :: thesis: verum