let n be Element of NAT ; :: thesis: for X, x being set
for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
let X, x be set ; :: thesis: for B being SetSequence of X holds
( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
let B be SetSequence of X; :: thesis: ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) )
A0: (superior_setsequence B) . n = union { (B . k) where k is Element of NAT : n <= k } by def3;
set Y = { (B . k) where k is Element of NAT : n <= k } ;
thus ( x in (superior_setsequence B) . n implies ex k being Element of NAT st x in B . (n + k) ) :: thesis: ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n )

proof

assume x in (superior_setsequence B) . n ; :: thesis: ex k being Element of NAT st x in B . (n + k)
then consider Y1 being set such that
AB: ( x in Y1 & Y1 in { (B . k) where k is Element of NAT : n <= k } ) by A0, TARSKI:def 4;
consider k11 being Element of NAT such that
AA2: ( Y1 = B . k11 & n <= k11 ) by AB;
ex k being Nat st k11 = n + k by AA2, NAT_1:10;
then consider k22 being Nat such that
AA3: Y1 = B . (n + k22) by AA2;
k22 in NAT by ORDINAL1:def 13;
hence ex k being Element of NAT st x in B . (n + k) by AB, AA3; :: thesis: verum

end;

now

assume ex k being Element of NAT st x in B . (n + k) ; :: thesis: x in (superior_setsequence B) . n
then consider k1 being Element of NAT such that
C0: x in B . (n + k1) ;
B . (n + k1) in { (B . k) where k is Element of NAT : n <= k } by Th5;
hence x in (superior_setsequence B) . n by A0, C0, TARSKI:def 4; :: thesis: verum

end;

hence ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n ) ; :: thesis: verum