let X be BCI-algebra; :: thesis: for A being Ideal of X st X is quasi-associative holds
A is closed
let A be Ideal of X; :: thesis: ( X is quasi-associative implies A is closed )
assume A0: X is quasi-associative ; :: thesis: A is closed
for x being Element of A holds x ` in A

proof

let x be Element of A; :: thesis: x ` in A
x ` <= x by A0, BCIALG_1:71;
hence x ` in A by P141; :: thesis: verum

end;

hence A is closed by BCIALG_1:def 19; :: thesis: verum