take f = S --> (Top T); :: thesis: f is infs-preserving
let A be Subset of S; :: according to WAYBEL_0:def 32 :: thesis: f preserves_inf_of A
assume ex_inf_of A,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: A,T & "/\" (f .: A),T = f . ("/\" A,S) )
A1: f = the carrier of S --> (Top T) ;
then ( rng f = {(Top T)} & f .: A c= rng f ) by FUNCOP_1:14, RELAT_1:144;
then A2: ( f .: A = {} or f .: A = {(Top T)} ) by ZFMISC_1:39;
hence ex_inf_of f .: A,T by YELLOW_0:38, YELLOW_0:43; :: thesis: "/\" (f .: A),T = f . ("/\" A,S)
thus inf (f .: A) = Top T by A2, YELLOW_0:39
.= f . (inf A) by A1, FUNCOP_1:13 ; :: thesis: verum