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;

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

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))

then A5:
A |^.. m c= (A |^ (m,n)) \/ (A |^.. (n + 1))
;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;

hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def 3; :: thesis: verum

end;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) )

( k <= n implies x in A |^ (m,n) )
by A2, A3, FLANG_2:19;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;then k >= n + 1 by NAT_1:13;

hence x in A |^.. (n + 1) by A3, Th2; :: thesis: verum

hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def 3; :: thesis: verum

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