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 X9 = 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: {a} c= (S --> a) .: X
proof
set n = the Element of X9;
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in {a} or b in (S --> a) .: X )
A2: a = ( the carrier of S --> a) . the Element of X9 by FUNCOP_1:7
.= (S --> a) . the Element of X9 ;
assume b in {a} ; :: thesis: b in (S --> a) .: X
then A3: b = a by TARSKI:def 1;
dom (S --> a) = the carrier of S by FUNCOP_1:13;
hence b in (S --> a) .: X by A3, A2, FUNCT_1:def 6; :: thesis: verum
end;
(S --> a) .: X c= rng (S --> a) by RELAT_1:111;
then (S --> a) .: X c= {a} by FUNCOP_1:8;
hence sup ((S --> a) .: X) = sup {a} by A1, XBOOLE_0:def 10
.= a by YELLOW_0:39
.= ( the carrier of S --> a) . (sup X) by FUNCOP_1:7
.= (S --> a) . (sup X) ;
:: thesis: verum
end;
hence S --> a preserves_sup_of X ; :: thesis: verum
end;
hence S --> a is directed-sups-preserving ; :: thesis: verum