let E be set ; :: thesis: for A, B being Subset of (E ^omega )
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^.. n c= B |^.. k
let A, B be Subset of (E ^omega ); :: thesis: for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^.. n c= B |^.. k
let k, n be Nat; :: thesis: ( A c= B |^.. k & n > 0 implies A |^.. n c= B |^.. k )
assume A1: ( A c= B |^.. k & n > 0 ) ; :: thesis: A |^.. n c= B |^.. k
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. n or x in B |^.. k )
assume x in A |^.. n ; :: thesis: x in B |^.. k
then consider m being Nat such that
A2: ( m >= n & x in A |^ m ) by Th2;
A |^ m c= B |^.. k by A1, A2, Th28;
hence x in B |^.. k by A2; :: thesis: verum