let X9, X be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for a being Element of X st a is atom holds
f . a is atom
let f be BCI-homomorphism of X,X9; :: thesis: for a being Element of X st a is atom holds
f . a is atom
let a be Element of X; :: thesis: ( a is atom implies f . a is atom )
assume a is atom ; :: thesis: f . a is atom
then f . a = f . ((a ` ) ` ) by BCIALG_2:29;
then f . a = (f . (0. X)) \ (f . ((0. X) \ a)) by Def6;
then f . a = (f . (0. X)) \ ((f . (0. X)) \ (f . a)) by Def6;
then f . a = ((f . (0. X)) \ (f . a)) ` by Th35;
then f . a = ((f . a) ` ) ` by Th35;
hence f . a is atom by BCIALG_2:29; :: thesis: verum