let X, X9 be BCI-algebra; :: thesis: for A9 being non empty Subset of X9
for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds
f " A9 is closed Ideal of X
let A9 be non empty Subset of X9; :: thesis: for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds
f " A9 is closed Ideal of X
let f be BCI-homomorphism of X,X9; :: thesis: ( A9 is closed Ideal of X9 implies f " A9 is closed Ideal of X )
assume A1: A9 is closed Ideal of X9 ; :: thesis: f " A9 is closed Ideal of X
then reconsider XY = f " A9 as Ideal of X by Th45;
for y being Element of XY holds y ` in XY

proof

let y be Element of XY; :: thesis: y ` in XY
A2: f . y in A9 by FUNCT_2:38;
reconsider y = y as Element of X ;
(f . y) ` in A9 by A1, A2, BCIALG_1:def 19;
then (f . (0. X)) \ (f . y) in A9 by Th35;
then f . (y `) in A9 by Def6;
hence y ` in XY by FUNCT_2:38; :: thesis: verum

end;

hence f " A9 is closed Ideal of X by BCIALG_1:def 19; :: thesis: verum