:: deftheorem Def3 defines superior_setsequence SETLIM_1:def 3 :
for B, b₂ being Function holds
( b₂ = superior_setsequence B iff ( dom b₂ = NAT & ( for n being Nat holds b₂ . n = union { (B . k) where k is Nat : n <= k } ) ) );