:: deftheorem Def2 defines inferior_setsequence SETLIM_1:def 2 :
for B, b₂ being Function holds
( b₂ = inferior_setsequence B iff ( dom b₂ = NAT & ( for n being Nat holds b₂ . n = meet { (B . k) where k is Nat : n <= k } ) ) );