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,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,n)
let m, k, n be Nat; :: thesis: ( m <= k & k <= n implies A |^ m,n = (A |^ m,k) \/ (A |^ k,n) )
A1: A |^ m,n c= (A |^ m,k) \/ (A |^ k,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,n) )
assume x in A |^ m,n ; :: thesis: x in (A |^ m,k) \/ (A |^ k,n)
then consider l being Nat such that
A2: ( m <= l & l <= n & x in A |^ l ) by Th19;
( l <= k or l > k ) ;
then ( x in A |^ m,k or x in A |^ k,n ) by A2, Th19;
hence x in (A |^ m,k) \/ (A |^ k,n) by XBOOLE_0:def 3; :: thesis: verum

end;

assume ( m <= k & k <= n ) ; :: thesis: A |^ m,n = (A |^ m,k) \/ (A |^ k,n)
then ( A |^ m,k c= A |^ m,n & A |^ k,n c= A |^ m,n ) by Th23;
then (A |^ m,k) \/ (A |^ k,n) c= A |^ m,n by XBOOLE_1:8;
hence A |^ m,n = (A |^ m,k) \/ (A |^ k,n) by A1, XBOOLE_0:def 10; :: thesis: verum