let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let A be Subset of (E ^omega); :: thesis: for m, n, k, l being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let m, n, k, l be Nat; :: thesis: (A |^ (m,n)) |^ (k,l) c= A *
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ (m,n)) |^ (k,l) or x in A * )
assume x in (A |^ (m,n)) |^ (k,l) ; :: thesis: x in A *
then consider kl being Nat such that
k <= kl and
kl <= l and
A1: x in (A |^ (m,n)) |^ kl by Th19;
(A |^ (m,n)) |^ kl c= A * by Th32, FLANG_1:59;
hence x in A * by A1; :: thesis: verum