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,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,n))
let k, m, n be Nat; ( 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 ;
TARSKI:def 3 ( not x in A |^ (m,n) or x in (A |^ (m,k)) \/ (A |^ (k,n)) )
assume
x in A |^ (
m,
n)
;
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;
verum
end;
assume
( m <= k & k <= n )
; 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; verum