let E be set ; :: thesis: for A, B being Subset of (E ^omega)

for n being Nat st A c= B holds

A |^.. n c= B |^.. n

let A, B be Subset of (E ^omega); :: thesis: for n being Nat st A c= B holds

A |^.. n c= B |^.. n

let n be Nat; :: thesis: ( A c= B implies A |^.. n c= B |^.. n )

assume A1: A c= B ; :: thesis: A |^.. n c= B |^.. n

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. n or x in B |^.. n )

assume x in A |^.. n ; :: thesis: x in B |^.. n

then consider k being Nat such that

A2: n <= k and

A3: x in A |^ k by Th2;

A |^ k c= B |^ k by A1, FLANG_1:37;

hence x in B |^.. n by A2, A3, Th2; :: thesis: verum

for n being Nat st A c= B holds

A |^.. n c= B |^.. n

let A, B be Subset of (E ^omega); :: thesis: for n being Nat st A c= B holds

A |^.. n c= B |^.. n

let n be Nat; :: thesis: ( A c= B implies A |^.. n c= B |^.. n )

assume A1: A c= B ; :: thesis: A |^.. n c= B |^.. n

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^.. n or x in B |^.. n )

assume x in A |^.. n ; :: thesis: x in B |^.. n

then consider k being Nat such that

A2: n <= k and

A3: x in A |^ k by Th2;

A |^ k c= B |^ k by A1, FLANG_1:37;

hence x in B |^.. n by A2, A3, Th2; :: thesis: verum