let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
let n be Nat; :: thesis:
{ (B . k1) where k1 is Nat : n <= k1 } = { (B . k2) where k2 is Nat : n + 1 <= k2 } \/ {(B . n)} by Th2;
then union { (B . k2) where k2 is Nat : n + 1 <= k2 } c= union { (B . k1) where k1 is Nat : n <= k1 } by XBOOLE_1:7, ZFMISC_1:77;
then (superior_setsequence B) . (n + 1) c= union { (B . k1) where k1 is Nat : n <= k1 } by Def3;
then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3;

A2: now :: thesis:

let x be object ; :: thesis:
assume A3: ( x in (superior_setsequence B) . (n + 1) or x in B . n ) ; :: thesis:
thus x in (superior_setsequence B) . n :: thesis:

proof

now :: thesis:

per cases by A3;

case x in (superior_setsequence B) . (n + 1) ; :: thesis:

hence x in (superior_setsequence B) . n by A1; :: thesis:

end;

case A4: x in B . n ; :: thesis:

B . n in { (B . k1) where k1 is Nat : n <= k1 } ;
then x in union { (B . k1) where k1 is Nat : n <= k1 } by A4, TARSKI:def 4;
hence x in (superior_setsequence B) . n by Def3; :: thesis:

end;

end;

end;

hence x in (superior_setsequence B) . n ; :: thesis:

end;

end;

now :: thesis:

let x be object ; :: thesis:
assume x in (superior_setsequence B) . n ; :: thesis:
then x in union { (B . k1) where k1 is Nat : n <= k1 } by Def3;
then consider Y1 being set such that
A5: ( x in Y1 & Y1 in { (B . k1) where k1 is Nat : n <= k1 } ) by TARSKI:def 4;
consider k11 being Nat such that
A6: ( Y1 = B . k11 & n <= k11 ) by A5;

now :: thesis:

per cases by A6, Lm1;

case ( Y1 = B . k11 & n = k11 ) ; :: thesis:

hence x in B . n by A5; :: thesis:

end;

case ( Y1 = B . k11 & n + 1 <= k11 ) ; :: thesis:

then Y1 in { (B . k2) where k2 is Nat : n + 1 <= k2 } ;
hence x in union { (B . k2) where k2 is Nat : n + 1 <= k2 } by A5, TARSKI:def 4; :: thesis:

end;

end;

end;

hence ( x in B . n or x in (superior_setsequence B) . (n + 1) ) by Def3; :: thesis:

end;

then for x being object holds
( x in (superior_setsequence B) . n iff ( x in B . n or x in (superior_setsequence B) . (n + 1) ) ) by A2;
hence (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by XBOOLE_0:def 3; :: thesis: