let E be set ; :: thesis: for A, B being Subset of (E ^omega )
for m, n being Nat st A c= B * holds
A |^ m,n c= B *
let A, B be Subset of (E ^omega ); :: thesis: for m, n being Nat st A c= B * holds
A |^ m,n c= B *
let m, n be Nat; :: thesis: ( A c= B * implies A |^ m,n c= B * )
assume A1: A c= B * ; :: thesis: A |^ m,n c= B *
thus A |^ m,n c= B * :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ m,n or x in B * )
assume x in A |^ m,n ; :: thesis: x in B *
then consider mn being Nat such that
m <= mn and
mn <= n and
A2: x in A |^ mn by Th19;
A |^ mn c= B * by A1, FLANG_1:60;
hence x in B * by A2; :: thesis: verum

end;