let S be non empty RelStr ; 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 ; S --> (Bottom T) is sups-preserving
let X be Subset of S; WAYBEL_0:def 33 S --> (Bottom T) preserves_sup_of X
assume
ex_sup_of X,S
; WAYBEL_0:def 31 ( 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; verum