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

proof

assume that
A1: <%> E in A |^ m,n and
A2: ( m <> 0 & ( m > n or not <%> E in A ) ) ; :: thesis: contradiction

per cases ( ( m <> 0 & m > n ) or ( m <> 0 & not <%> E in A ) ) by A2;

suppose ( m <> 0 & m > n ) ; :: thesis: contradiction

hence contradiction by A1, Th21; :: thesis: verum

end;

suppose A3: ( m <> 0 & not <%> E in A ) ; :: thesis: contradiction

consider k being Nat such that
A4: ( m <= k & k <= n & <%> E in A |^ k ) by A1, Th19;
k > 0 by A3, A4;
hence contradiction by A3, A4, FLANG_1:32; :: thesis: verum

end;

end;

end;

assume A5: ( m = 0 or ( m <= n & <%> E in A ) ) ; :: thesis: <%> E in A |^ m,n

per cases ( m = 0 or ( m <= n & <%> E in A ) ) by A5;

suppose A6: m = 0 ; :: thesis: <%> E in A |^ m,n

{(<%> E)} = A |^ 0 by FLANG_1:30;
then ( {(<%> E)} c= A |^ 0 ,n & <%> E in {(<%> E)} ) by Th20, TARSKI:def 1;
hence <%> E in A |^ m,n by A6; :: thesis: verum

end;

suppose A7: ( m <= n & <%> E in A ) ; :: thesis: <%> E in A |^ m,n

then A8: <%> E in A |^ m by FLANG_1:31;
A |^ m c= A |^ m,n by A7, Th20;
hence <%> E in A |^ m,n by A8; :: thesis: verum

end;

end;