theorem Th29: :: WAYBEL21:29

for S, T being non empty /\-complete Poset
for X being non empty filtered Subset of S
for f being monotone Function of S,T holds lim_inf (f * (X opp+id)) = inf (f .: X)