let E be set ; :: thesis: for A being Subset of ()
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m

let A be Subset of (); :: 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 ; :: thesis: verum
end;
( k <= n implies x in A |^ (m,n) ) by ;
hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by ; :: 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 ;
hence (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m by ; :: thesis: verum