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
f * (X opp+id) is subnet of Y opp+id