let x be object ; :: thesis:
let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
let n be Nat; :: thesis:
set Y = { (B . k) where k is Nat : n <= k } ;
A1: (superior_setsequence B) . n = union { (B . k) where k is Nat : n <= k } by Def3;
thus ( x in (superior_setsequence B) . n implies ex k being Nat st x in B . (n + k) ) :: thesis:

assume x in (superior_setsequence B) . n ; :: thesis:
then consider Y1 being set such that
A2: x in Y1 and
A3: Y1 in { (B . k) where k is Nat : n <= k } by A1, TARSKI:def 4;
consider k11 being Nat such that
A4: Y1 = B . k11 and
A5: n <= k11 by A3;
ex k being Nat st k11 = n + k by A5, NAT_1:10;
then consider k22 being Nat such that
A6: Y1 = B . (n + k22) by A4;
thus ex k being Nat st x in B . (n + k) by A2, A6; :: thesis:

end;

given k1 being Nat such that A7: x in B . (n + k1) ; :: thesis:
B . (n + k1) in { (B . k) where k is Nat : n <= k } by Th1;
hence x in (superior_setsequence B) . n by A1, A7, TARSKI:def 4; :: thesis:

end;