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

for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

let A be Subset of (E ^omega); :: thesis: for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

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

assume A1: m > 0 ; :: thesis: A |^ (m,n) c= A +

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

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

then ex k being Nat st

( m <= k & k <= n & x in A |^ k ) by FLANG_2:19;

hence x in A + by A1, Th48; :: thesis: verum

for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

let A be Subset of (E ^omega); :: thesis: for m, n being Nat st m > 0 holds

A |^ (m,n) c= A +

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

assume A1: m > 0 ; :: thesis: A |^ (m,n) c= A +

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

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

then ex k being Nat st

( m <= k & k <= n & x in A |^ k ) by FLANG_2:19;

hence x in A + by A1, Th48; :: thesis: verum