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: verum

proof

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) )
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 ; :: thesis: "/\" (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; :: thesis: verum

end;

end;

assume A3: 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) )
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 ; :: thesis: "\/" (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; :: thesis: verum