let S, T be non empty TopPoset; :: thesis: 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))
let X be non empty filtered Subset of S; :: thesis: 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))
let f be monotone Function of S,T; :: thesis: for Y being non empty filtered Subset of T st Y = f .: X holds
Lim (Y opp+id) c= Lim (f * (X opp+id))
let Y be non empty filtered Subset of T; :: thesis: ( Y = f .: X implies Lim (Y opp+id) c= Lim (f * (X opp+id)) )
assume Y = f .: X ; :: thesis: Lim (Y opp+id) c= Lim (f * (X opp+id))
then f * (X opp+id) is subnet of Y opp+id by Th30;
hence Lim (Y opp+id) c= Lim (f * (X opp+id)) by YELLOW_6:32; :: thesis: verum