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:8;
f .: A c= rng f by RELAT_1:111;
then A2: ( f .: A = {} or f .: A = {(Top T)} ) by A1, ZFMISC_1:33;
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:7 ; :: thesis: verum