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 object ; :: 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:59;
hence x in B * by A2; :: thesis: verum

end;