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 S1[ Nat] means (B \/ A) |^ $1 c= B * ;
assume A1: A c= B * ; :: thesis: B * = (B \/ A) *
A2: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[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 S1[n + 1] by A3, A4, Th46; :: thesis: verum
end;
( (B \/ A) |^ 0 = {(<%> E)} & <%> E in B * ) by Th24, Th48;
then A5: S1[ 0 ] by ZFMISC_1:31;
A6: for n being Nat holds S1[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