let E be set ; for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let A be Subset of (E ^omega); for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A *
let k, l, m, n be Nat; (A |^ (m,n)) |^ (k,l) c= A *
let x be object ; TARSKI:def 3 ( not x in (A |^ (m,n)) |^ (k,l) or x in A * )
assume
x in (A |^ (m,n)) |^ (k,l)
; 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; verum