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

for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m

let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m

let m, n be Nat; :: thesis: (A +) |^ (m,n) c= A |^.. m

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

assume x in (A +) |^ (m,n) ; :: thesis: x in A |^.. m

then consider k being Nat such that

A1: m <= k and

k <= n and

A2: x in (A +) |^ k by FLANG_2:19;

(A +) |^ k c= A |^.. k by Th87;

then A3: x in A |^.. k by A2;

A |^.. k c= A |^.. m by A1, Th5;

hence x in A |^.. m by A3; :: thesis: verum

for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m

let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m

let m, n be Nat; :: thesis: (A +) |^ (m,n) c= A |^.. m

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

assume x in (A +) |^ (m,n) ; :: thesis: x in A |^.. m

then consider k being Nat such that

A1: m <= k and

k <= n and

A2: x in (A +) |^ k by FLANG_2:19;

(A +) |^ k c= A |^.. k by Th87;

then A3: x in A |^.. k by A2;

A |^.. k c= A |^.. m by A1, Th5;

hence x in A |^.. m by A3; :: thesis: verum