let L be non empty Poset; for p being Function of L,L holds
( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
let p be Function of L,L; ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
hereby ( p is kernel implies Image p is sups-inheriting )
assume A1:
p is
closure
;
Image p is infs-inheriting thus
Image p is
infs-inheriting
verumproof
let X be
Subset of
(Image p);
YELLOW_0:def 18 ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) )
A2:
the
carrier of
(Image p) = rng p
by YELLOW_0:def 15;
then reconsider X9 =
X as
Subset of
L by XBOOLE_1:1;
assume
ex_inf_of X,
L
;
"/\" (X,L) in the carrier of (Image p)
then
p . ("/\" (X9,L)) = "/\" (
X9,
L)
by A1, A2, Th28;
hence
"/\" (
X,
L)
in the
carrier of
(Image p)
by A2, FUNCT_2:4;
verum
end;
end;
assume A3:
p is kernel
; Image p is sups-inheriting
let X be Subset of (Image p); YELLOW_0:def 19 ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) )
A4:
the carrier of (Image p) = rng p
by YELLOW_0:def 15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume
ex_sup_of X,L
; "\/" (X,L) in the carrier of (Image p)
then
p . ("\/" (X9,L)) = "\/" (X9,L)
by A3, A4, Th29;
hence
"\/" (X,L) in the carrier of (Image p)
by A4, FUNCT_2:4; verum