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) )
set Y = { (B . k) where k is Element of NAT : n <= k } ;
A1: (superior_setsequence B) . n = union { (B . k) where k is Element of NAT : n <= k } by Def3;
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
A2: x in Y1 and
A3: Y1 in { (B . k) where k is Element of NAT : n <= k } by A1, TARSKI:def 4;
consider k11 being Element of 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;
k22 in NAT by ORDINAL1:def 12;
hence ex k being Element of NAT st x in B . (n + k) by A2, A6; :: 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
A7: x in B . (n + k1) ;
B . (n + k1) in { (B . k) where k is Element of NAT : n <= k } by Th1;
hence x in (superior_setsequence B) . n by A1, A7, 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