let x be object ; :: thesis: for X being set

for B being SetSequence of X

for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let X be set ; :: thesis: for B being SetSequence of X

for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let B be SetSequence of X; :: thesis: for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let n be Nat; :: thesis: ( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

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: ( ex k being Nat st x in B . (n + k) implies x in (superior_setsequence B) . n )

for B being SetSequence of X

for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let X be set ; :: thesis: for B being SetSequence of X

for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let B be SetSequence of X; :: thesis: for n being Nat holds

( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

let n be Nat; :: thesis: ( x in (superior_setsequence B) . n iff ex k being Nat st x in B . (n + k) )

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: ( ex k being 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 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 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: verum

end;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: verum

now :: thesis: ( ex k1 being Nat st x in B . (n + k1) implies x in (superior_setsequence B) . n )

hence
( ex k being Nat st x in B . (n + k) implies x in (superior_setsequence B) . n )
; :: thesis: verumgiven k1 being Nat such that A7:
x in B . (n + k1)
; :: thesis: x in (superior_setsequence B) . n

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: verum

end;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: verum