let L be non empty up-complete Poset; for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
Image f is directed-sups-inheriting
let f be Function of L,L; ( f is idempotent & f is directed-sups-preserving implies Image f is directed-sups-inheriting )
set S = subrelstr (rng f);
set a = the Element of L;
reconsider S9 = subrelstr (rng f) as non empty full SubRelStr of L ;
assume A1:
( f is idempotent & f is directed-sups-preserving )
; Image f is directed-sups-inheriting
subrelstr (rng f) is directed-sups-inheriting
proof
let X be
directed Subset of
(subrelstr (rng f));
WAYBEL_0:def 4 ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
X c= the
carrier of
(subrelstr (rng f))
;
then A2:
X c= rng f
by YELLOW_0:def 15;
assume
X <> {}
;
( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
then
X is non
empty directed Subset of
S9
;
then reconsider X9 =
X as non
empty directed Subset of
L by YELLOW_2:7;
assume A3:
ex_sup_of X,
L
;
"\/" (X,L) in the carrier of (subrelstr (rng f))
f preserves_sup_of X9
by A1;
then
sup (f .: X9) = f . (sup X9)
by A3;
then
sup X9 = f . (sup X9)
by A1, A2, YELLOW_2:20;
then
"\/" (
X,
L)
in rng f
by FUNCT_2:4;
hence
"\/" (
X,
L)
in the
carrier of
(subrelstr (rng f))
by YELLOW_0:def 15;
verum
end;
hence
Image f is directed-sups-inheriting
; verum