theorem :: WAYBEL21:31

for S, T being non empty TopPoset
for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))