let E be set ; :: thesis:
let A be Subset of (E ^omega); :: thesis:
let m, n be Nat; :: thesis:

A1: now :: thesis:

assume A2: ( m > 0 & A = {} ) ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in A |^ (m,n) ; :: thesis:
then ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by Th19;
hence contradiction by A2, FLANG_1:27; :: thesis:

end;

hence A |^ (m,n) = {} by XBOOLE_0:def 1; :: thesis:

end;

thus ( not A |^ (m,n) = {} or m > n or ( m > 0 & A = {} ) ) :: thesis:

proof

assume that
A3: A |^ (m,n) = {} and
A4: ( m <= n & ( m <= 0 or A <> {} ) ) ; :: thesis:

A5: now :: thesis:

assume that
A6: m <= n and
A7: A <> {} ; :: thesis:
A |^ m <> {} by A7, FLANG_1:27;
then ex a being Element of E ^omega st a in A |^ m by SUBSET_1:4;
hence contradiction by A3, A6, Th19; :: thesis:

end;

now :: thesis:

assume that
A8: m <= n and
A9: m = 0 ; :: thesis:
{(<%> E)} = A |^ m by A9, FLANG_1:29;
then <%> E in A |^ m by TARSKI:def 1;
hence contradiction by A3, A8, Th19; :: thesis:

end;

hence contradiction by A4, A5; :: thesis:

end;

now :: thesis:

assume A10: m > n ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
for k being Nat holds
( not m <= k or not k <= n or not x in A |^ k ) by A10, XXREAL_0:2;
hence not x in A |^ (m,n) by Th19; :: thesis:

end;

hence A |^ (m,n) = {} by XBOOLE_0:def 1; :: thesis:

end;

hence ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ (m,n) = {} ) by A1; :: thesis: