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: rng f = {(Top T)} by FUNCOP_1:14;
f .: A c= rng f by RELAT_1:144;
then A2: ( f .: A = {} or f .: A = {(Top T)} ) by A1, 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 FUNCOP_1:13 ; :: thesis: verum