theorem Th15: :: SETLIM_1:15

for X being set
for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Nat holds f . n = meet { (B . k) where k is Nat : n <= k } ) holds
f is SetSequence of X