let X be BCI-algebra; :: thesis: ( AtomSet X is Ideal of X implies AtomSet X is closed Ideal of X )
set P = AtomSet X;
A1: for x being Element of AtomSet X holds x ` in AtomSet X

proof

let x be Element of AtomSet X; :: thesis: x ` in AtomSet X
x ` is minimal by BCIALG_2:30;
hence x ` in AtomSet X ; :: thesis: verum

end;

assume AtomSet X is Ideal of X ; :: thesis: AtomSet X is closed Ideal of X
hence AtomSet X is closed Ideal of X by A1, BCIALG_1:def 19; :: thesis: verum