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 that

A1: A c= B |^.. k and

A2: n > 0 ; :: thesis: A |^.. n c= B |^.. k

let x be object ; :: 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

A3: m >= n and

A4: x in A |^ m by Th2;

A |^ m c= B |^.. k by A1, A2, A3, Th28;

hence x in B |^.. k by A4; :: thesis: verum

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 that

A1: A c= B |^.. k and

A2: n > 0 ; :: thesis: A |^.. n c= B |^.. k

let x be object ; :: 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

A3: m >= n and

A4: x in A |^ m by Th2;

A |^ m c= B |^.. k by A1, A2, A3, Th28;

hence x in B |^.. k by A4; :: thesis: verum