set f = S --> a;
for X being Subset of S st not X is empty & X is directed holds
S --> a preserves_sup_of X

proof

let X be Subset of S; :: thesis: ( not X is empty & X is directed implies S --> a preserves_sup_of X )
assume ( not X is empty & X is directed ) ; :: thesis: S --> a preserves_sup_of X
then reconsider X' = X as non empty directed Subset of S ;
S --> a preserves_sup_of X

proof

assume ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (S --> a) .: X,T & "\/" ((S --> a) .: X),T = (S --> a) . ("\/" X,S) )
thus ex_sup_of (S --> a) .: X,T by YELLOW_0:17; :: thesis: "\/" ((S --> a) .: X),T = (S --> a) . ("\/" X,S)
A1: (S --> a) .: X c= rng (S --> a) by RELAT_1:144;
A2: S --> a = the carrier of S --> a by BORSUK_1:def 2;
then A3: (S --> a) .: X c= {a} by A1, FUNCOP_1:14;
{a} c= (S --> a) .: X

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in {a} or b in (S --> a) .: X )
assume b in {a} ; :: thesis: b in (S --> a) .: X
then A4: b = a by TARSKI:def 1;
consider n being Element of X';
A5: dom (S --> a) = the carrier of S by A2, FUNCOP_1:19;
a = (the carrier of S --> a) . n by FUNCOP_1:13
.= (S --> a) . n by BORSUK_1:def 2 ;
hence b in (S --> a) .: X by A4, A5, FUNCT_1:def 12; :: thesis: verum

end;

hence sup ((S --> a) .: X) = sup {a} by A3, XBOOLE_0:def 10
.= a by YELLOW_0:39
.= (the carrier of S --> a) . (sup X) by FUNCOP_1:13
.= (S --> a) . (sup X) by BORSUK_1:def 2 ;
:: thesis: verum

end;

hence S --> a preserves_sup_of X ; :: thesis: verum

end;

hence S --> a is directed-sups-preserving by WAYBEL_0:def 37; :: thesis: verum