let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds S --> (Bottom T) is sups-preserving
let T be non empty reflexive antisymmetric lower-bounded RelStr ; :: 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)) )
set f = the carrier of S --> (Bottom T);
A1: ( the carrier of S --> (Bottom T)) . (sup X) = Bottom T by FUNCOP_1:7;
(S --> (Bottom T)) .: X c= {(Bottom T)} by FUNCOP_1:81;
then ( (S --> (Bottom T)) .: X = {(Bottom T)} or (S --> (Bottom T)) .: X = {} ) by ZFMISC_1:33;
hence ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) ) by A1, YELLOW_0:38, YELLOW_0:39, YELLOW_0:42; :: thesis: verum