thus S --> (Top T) is directed-sups-preserving :: thesis: S --> (Top T) is infs-preserving

proof

let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or S --> (Top T) preserves_sup_of X )
thus ( X is empty or not X is directed or S --> (Top T) preserves_sup_of X ) by Th44; :: thesis: verum

end;

thus S --> (Top T) is infs-preserving by Th46; :: thesis: verum