take f = S --> (Bottom T); :: thesis: f is sups-preserving
let A be Subset of ; :: 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: rng f = {(Bottom T)} by FUNCOP_1:14;
f .: A c= rng f by RELAT_1:144;
then A2: ( f .: A = {} or f .: A = {(Bottom T)} ) by A1, 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 FUNCOP_1:13 ; :: thesis: verum