set t = Bottom T;
set f = S --> (Bottom T);
take S --> (Bottom T) ; :: thesis: S --> (Bottom T) is sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def 33 :: thesis: S --> (Bottom T) preserves_sup_of X
assume ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" ((S --> (Bottom T)) .: X),T = (S --> (Bottom T)) . ("\/" X,S) )
thus ex_sup_of (S --> (Bottom T)) .: X,T by YELLOW_0:17; :: thesis: "\/" ((S --> (Bottom T)) .: X),T = (S --> (Bottom T)) . ("\/" X,S)
A1: (S --> (Bottom T)) .: X c= rng (S --> (Bottom T)) by RELAT_1:144;
A2: S --> (Bottom T) = the carrier of S --> (Bottom T) ;
then rng (S --> (Bottom T)) c= {(Bottom T)} by FUNCOP_1:19;
then (S --> (Bottom T)) .: X c= {(Bottom T)} by A1, XBOOLE_1:1;
then A3: ( (S --> (Bottom T)) .: X = {(Bottom T)} or (S --> (Bottom T)) .: X = {} ) by ZFMISC_1:39;

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: "\/" ((S --> (Bottom T)) .: X),T = (S --> (Bottom T)) . ("\/" X,S)

then (S --> (Bottom T)) .: X = {} by RELAT_1:149;
then sup ((S --> (Bottom T)) .: X) = Bottom T by YELLOW_0:def 11;
hence "\/" ((S --> (Bottom T)) .: X),T = (S --> (Bottom T)) . ("\/" X,S) by A2, FUNCOP_1:13; :: thesis: verum

end;

suppose X <> {} ; :: thesis: "\/" ((S --> (Bottom T)) .: X),T = (S --> (Bottom T)) . ("\/" X,S)

then reconsider X1 = X as non empty Subset of S ;
consider x being Element of X1;
(S --> (Bottom T)) . x in (S --> (Bottom T)) .: X by FUNCT_2:43;
hence sup ((S --> (Bottom T)) .: X) = Bottom T by A3, YELLOW_0:39
.= (S --> (Bottom T)) . (sup X) by A2, FUNCOP_1:13 ;
:: thesis: verum

end;

end;