let E be set ; 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); 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; ( m <= k & k <= n implies A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n)) )
assume that
A1:
m <= k
and
A2:
k <= n
; A |^ (m,n) = (A |^ (m,k)) \/ (A |^ ((k + 1),n))
per cases
( k < n or k >= n )
;
suppose A3:
k < n
;
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 ;
TARSKI:def 3 ( not x in A |^ (m,n) or x in (A |^ (m,k)) \/ (A |^ ((k + 1),n)) )
assume
x in A |^ (
m,
n)
;
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;
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;
verum end; end;