let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds
( A |^ m,n = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds
( A |^ m,n = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let m, n be Nat; :: thesis: ( A |^ m,n = {} iff ( m > n or ( m > 0 & A = {} ) ) )
thus ( not A |^ m,n = {} or m > n or ( m > 0 & A = {} ) ) :: thesis: ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ m,n = {} )

proof

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

A3: now

assume A4: ( m <= n & m = 0 ) ; :: thesis: contradiction
then {(<%> E)} = A |^ m by FLANG_1:30;
then <%> E in A |^ m by TARSKI:def 1;
hence contradiction by A1, A4, Th19; :: thesis: verum

end;

now

assume A5: ( m <= n & A <> {} ) ; :: thesis: contradiction
then A |^ m <> {} by FLANG_1:28;
then ex a being Element of E ^omega st a in A |^ m by SUBSET_1:10;
hence contradiction by A1, A5, Th19; :: thesis: verum

end;

hence contradiction by A2, A3; :: thesis: verum

end;

A6: now

assume A7: m > n ; :: thesis: A |^ m,n = {}

now

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

end;

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

end;

now

assume A8: ( m > 0 & A = {} ) ; :: thesis: A |^ m,n = {}

now

let x be set ; :: thesis: not x in A |^ m,n
assume x in A |^ m,n ; :: thesis: contradiction
then consider k being Nat such that
A9: ( m <= k & k <= n & x in A |^ k ) by Th19;
thus contradiction by A8, A9, FLANG_1:28; :: thesis: verum

end;

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

end;

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