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) * )
assume A1: A c= B * ; :: thesis: B * = (B \/ A) *
defpred S₁[ Nat] means (B \/ A) |^ $1 c= B * ;
A2: S₁[ 0 ]

proof

A3: (B \/ A) |^ 0 = {(<%> E)} by Th25;
<%> E in B * by Th49;
hence S₁[ 0 ] by A3, ZFMISC_1:37; :: thesis: verum

end;

A4: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: (B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by Th24;
B c= B * by Th44;
then B \/ A c= B * by A1, XBOOLE_1:8;
hence S₁[n + 1] by A5, A6, Th47; :: thesis: verum

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
A8: (B \/ A) * c= B *

proof

let x be set ; :: 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
A9: x in (B \/ A) |^ n by Th42;
(B \/ A) |^ n c= B * by A7;
hence x in B * by A9; :: thesis: verum

end;

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