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 |^ (m,n)
let A, B be Subset of (E ^omega); :: thesis: for m, n being Nat st A c= B holds
A |^ (m,n) c= B |^ (m,n)
let m, n be Nat; :: thesis: ( A c= B implies A |^ (m,n) c= B |^ (m,n) )
assume A1: A c= B ; :: thesis: A |^ (m,n) c= B |^ (m,n)
thus A |^ (m,n) c= B |^ (m,n) :: thesis: verum

proof

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

end;