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:41; :: thesis: verum