thus S --> (Bottom T) is filtered-infs-preserving :: thesis: S --> (Bottom T) is sups-preserving

proof

let X be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or S --> (Bottom T) preserves_inf_of X )
thus ( X is empty or not X is filtered or S --> (Bottom T) preserves_inf_of X ) by Th44; :: thesis: verum

end;

thus S --> (Bottom T) is sups-preserving by Th45; :: thesis: verum