let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat st <%> E in A & m <= n holds
A |^ m,n = A |^ n
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st <%> E in A & m <= n holds
A |^ m,n = A |^ n
let m, n be Nat; :: thesis: ( <%> E in A & m <= n implies A |^ m,n = A |^ n )
assume that
A1: <%> E in A and
A2: m <= n ; :: thesis: A |^ m,n = A |^ n
A3: A |^ m,n c= A |^ n

proof

A4: now

let k be Nat; :: thesis: ( k <= n implies A |^ b₁ c= A |^ n )
assume A5: k <= n ; :: thesis: A |^ b₁ c= A |^ n

per cases ( k < n or k = n ) by A5, XXREAL_0:1;

suppose k < n ; :: thesis: A |^ b₁ c= A |^ n

hence A |^ k c= A |^ n by A1, FLANG_1:37; :: thesis: verum

end;

suppose k = n ; :: thesis: A |^ b₁ c= A |^ n

hence A |^ k c= A |^ n ; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ m,n or x in A |^ n )
assume x in A |^ m,n ; :: thesis: x in A |^ n
then consider k being Nat such that
m <= k and
A6: k <= n and
A7: x in A |^ k by Th19;
A |^ k c= A |^ n by A4, A6;
hence x in A |^ n by A7; :: thesis: verum

end;

A |^ n c= A |^ m,n by A2, Th20;
hence A |^ m,n = A |^ n by A3, XBOOLE_0:def 10; :: thesis: verum