let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds (A + ) |^ m,n c= A |^.. m
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds (A + ) |^ m,n c= A |^.. m
let m, n be Nat; :: thesis: (A + ) |^ m,n c= A |^.. m
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A + ) |^ m,n or x in A |^.. m )
assume x in (A + ) |^ m,n ; :: thesis: x in A |^.. m
then consider k being Nat such that
A1: m <= k and
k <= n and
A2: x in (A + ) |^ k by FLANG_2:19;
(A + ) |^ k c= A |^.. k by Th87;
then A3: x in A |^.. k by A2;
A |^.. k c= A |^.. m by A1, Th5;
hence x in A |^.. m by A3; :: thesis: verum