let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, m, 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 k, m, n being Nat st m <= k & k <= n holds
A |^ (m,n) = (A |^ (m,k)) \/ (A |^ (k,n))
let k, m, 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 object ; :: 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