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

for k, m, n being Nat st k <= m holds

A |^ (m,n) c= A |^.. k

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

A |^ (m,n) c= A |^.. k

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

assume A1: k <= m ; :: thesis: A |^ (m,n) c= A |^.. k

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

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

then consider l being Nat such that

A2: m <= l and

l <= n and

A3: x in A |^ l by FLANG_2:19;

k <= l by A1, A2, XXREAL_0:2;

hence x in A |^.. k by A3, Th2; :: thesis: verum

for k, m, n being Nat st k <= m holds

A |^ (m,n) c= A |^.. k

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

A |^ (m,n) c= A |^.. k

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

assume A1: k <= m ; :: thesis: A |^ (m,n) c= A |^.. k

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

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

then consider l being Nat such that

A2: m <= l and

l <= n and

A3: x in A |^ l by FLANG_2:19;

k <= l by A1, A2, XXREAL_0:2;

hence x in A |^.. k by A3, Th2; :: thesis: verum