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 + 1),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 + 1),n))
let k, m, 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 object ; :: 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:8;
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;