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

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

set P = AtomSet X;

A1: for x being Element of AtomSet X holds x ` in AtomSet X

proof

assume
AtomSet X is Ideal of X
; :: thesis: AtomSet X is closed Ideal of X
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;x ` is minimal by BCIALG_2:30;

hence x ` in AtomSet X ; :: thesis: verum

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