let L be non empty Poset; :: thesis: 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; :: thesis: ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
hereby :: thesis: ( p is kernel implies Image p is sups-inheriting )
assume A1:
p is
closure
;
:: thesis: Image p is infs-inheriting thus
Image p is
infs-inheriting
:: thesis: verumproof
let X be
Subset of
(Image p);
:: according to YELLOW_0:def 18 :: thesis: ( not ex_inf_of X,L or "/\" X,L in the carrier of (Image p) )
assume A2:
ex_inf_of X,
L
;
:: thesis: "/\" X,L in the carrier of (Image p)
A3:
the
carrier of
(Image p) = rng p
by YELLOW_0:def 15;
then reconsider X' =
X as
Subset of
L by XBOOLE_1:1;
p . ("/\" X',L) = "/\" X',
L
by A1, A2, A3, Th30;
hence
"/\" X,
L in the
carrier of
(Image p)
by A3, FUNCT_2:6;
:: thesis: verum
end;
end;
assume A4:
p is kernel
; :: thesis: Image p is sups-inheriting
let X be Subset of (Image p); :: according to YELLOW_0:def 19 :: thesis: ( not ex_sup_of X,L or "\/" X,L in the carrier of (Image p) )
assume A5:
ex_sup_of X,L
; :: thesis: "\/" X,L in the carrier of (Image p)
A6:
the carrier of (Image p) = rng p
by YELLOW_0:def 15;
then reconsider X' = X as Subset of L by XBOOLE_1:1;
p . ("\/" X',L) = "\/" X',L
by A4, A5, A6, Th31;
hence
"\/" X,L in the carrier of (Image p)
by A6, FUNCT_2:6; :: thesis: verum