let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, k, n being Nat st m <= k & k <= n holds
A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n)
let A be Subset of (E ^omega ); :: thesis: for m, k, n being Nat st m <= k & k <= n holds
A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n)
let m, k, n be Nat; :: thesis: ( m <= k & k <= n implies A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n) )
assume that
A1: m <= k and
A2: k <= n ; :: thesis: A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n)

per cases ( k < n or k >= n ) ;

suppose A3: k < n ; :: thesis: A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n)

m <= k + 1 by A1, NAT_1:13;
then A4: A |^ (k + 1),n c= A |^ m,n by Th23;
A5: A |^ m,n c= (A |^ m,k) \/ (A |^ (k + 1),n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ m,n or x in (A |^ m,k) \/ (A |^ (k + 1),n) )
assume x in A |^ m,n ; :: thesis: x in (A |^ m,k) \/ (A |^ (k + 1),n)
then consider mn being Nat such that
A6: m <= mn and
A7: mn <= n and
A8: x in A |^ mn by Th19;
A9: ( mn >= k + 1 implies x in A |^ (k + 1),n ) by A7, A8, Th19;
( mn <= k implies x in A |^ m,k ) by A6, A8, Th19;
hence x in (A |^ m,k) \/ (A |^ (k + 1),n) by A9, NAT_1:13, XBOOLE_0:def 3; :: thesis: verum

end;

A |^ m,k c= A |^ m,n by A3, Th23;
then (A |^ m,k) \/ (A |^ (k + 1),n) c= A |^ m,n by A4, XBOOLE_1:8;
hence A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n) by A5, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A10: k >= n ; :: thesis: A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n)

then k + 1 > n + 0 by XREAL_1:10;
then A |^ (k + 1),n = {} by Th21;
hence A |^ m,n = (A |^ m,k) \/ (A |^ (k + 1),n) by A2, A10, XXREAL_0:1; :: thesis: verum

end;

end;