thus ( f is directed-sups-preserving implies for X being non empty directed Subset of S holds f preserves_sup_of X ) by WAYBEL_0:def 37; :: thesis: ( ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )
assume A1: for X being non empty directed Subset of S holds f preserves_sup_of X ; :: thesis: f is directed-sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or f preserves_sup_of X )
thus ( X is empty or not X is directed or f preserves_sup_of X ) by A1; :: thesis: verum