let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
let A be Subset of (E ^omega); :: thesis: for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
let m, n be Nat; :: thesis: ( m <= n + 1 implies (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m )
assume m <= n + 1 ; :: thesis: (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
then A1: A |^.. (n + 1) c= A |^.. m by Th5;
now :: thesis: for x being object st x in A |^.. m holds
x in (A |^ (m,n)) \/ (A |^.. (n + 1))
let x be object ; :: thesis: ( x in A |^.. m implies x in (A |^ (m,n)) \/ (A |^.. (n + 1)) )
assume x in A |^.. m ; :: thesis: x in (A |^ (m,n)) \/ (A |^.. (n + 1))
then consider k being Nat such that
A2: m <= k and
A3: x in A |^ k by Th2;
A4: now :: thesis: ( k > n implies x in A |^.. (n + 1) )
assume k > n ; :: thesis: x in A |^.. (n + 1)
then k >= n + 1 by NAT_1:13;
hence x in A |^.. (n + 1) by A3, Th2; :: thesis: verum
end;
( k <= n implies x in A |^ (m,n) ) by A2, A3, FLANG_2:19;
hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def 3; :: thesis: verum
end;
then A5: A |^.. m c= (A |^ (m,n)) \/ (A |^.. (n + 1)) ;
A |^ (m,n) c= A |^.. m by Th6;
then (A |^ (m,n)) \/ (A |^.. (n + 1)) c= A |^.. m by A1, XBOOLE_1:8;
hence (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m by A5, XBOOLE_0:def 10; :: thesis: verum