take f = S --> (Bottom T); :: thesis: f is sups-preserving
let A be Subset of S; :: according to WAYBEL_0:def 33 :: thesis: f preserves_sup_of A
assume ex_sup_of A,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: A,T & "\/" (f .: A),T = f . ("\/" A,S) )
A1: f = the carrier of S --> (Bottom T) ;
then ( rng f = {(Bottom T)} & f .: A c= rng f ) by FUNCOP_1:14, RELAT_1:144;
then A2: ( f .: A = {} or f .: A = {(Bottom T)} ) by ZFMISC_1:39;
hence ex_sup_of f .: A,T by YELLOW_0:38, YELLOW_0:42; :: thesis: "\/" (f .: A),T = f . ("\/" A,S)
thus sup (f .: A) = Bottom T by A2, YELLOW_0:39
.= f . (sup A) by A1, FUNCOP_1:13 ; :: thesis: verum