let X be associative BCI-algebra; :: thesis: for A being Ideal of X holds A is closed

let A be Ideal of X; :: thesis: A is closed

for x being Element of A holds x ` in A

let A be Ideal of X; :: thesis: A is closed

for x being Element of A holds x ` in A

proof

hence
A is closed
; :: thesis: verum
let x be Element of A; :: thesis: x ` in A

(0. X) \ x = x \ (0. X) by BCIALG_1:48

.= x by BCIALG_1:2 ;

hence x ` in A ; :: thesis: verum

end;(0. X) \ x = x \ (0. X) by BCIALG_1:48

.= x by BCIALG_1:2 ;

hence x ` in A ; :: thesis: verum