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 & sup (f .: A) = f . (sup A) )
A1: rng f = {(Bottom T)} by FUNCOP_1:8;
f .: A c= rng f by RELAT_1:111;
then A2: ( f .: A = {} or f .: A = {(Bottom T)} ) by A1, ZFMISC_1:33;
hence ex_sup_of f .: A,T by YELLOW_0:38, YELLOW_0:42; :: thesis: sup (f .: A) = f . (sup A)
thus sup (f .: A) = Bottom T by A2, YELLOW_0:39
.= f . (sup A) by FUNCOP_1:7 ; :: thesis: verum