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

proof

let y be Element of XY; :: thesis: y ` in XY
B1: f . y in A' by FUNCT_2:46;
reconsider y = y as Element of X ;
(f . y) ` in A' by A1, B1, BCIALG_1:def 19;
then (f . (0. X)) \ (f . y) in A' by PR1621;
then f . (y ` ) in A' by Def0;
hence y ` in XY by FUNCT_2:46; :: thesis: verum

end;

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