let X be BCI-algebra; :: thesis: for I being Ideal of X
for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
let RI be I-congruence of X,I; :: thesis: ( I is closed iff I = Class (RI,(0. X)) )
thus ( I is closed implies I = Class (RI,(0. X)) ) :: thesis: ( I = Class (RI,(0. X)) implies I is closed )

proof

assume A1: I is closed ; :: thesis: I = Class (RI,(0. X))
thus I c= Class (RI,(0. X)) :: according to XBOOLE_0:def 10 :: thesis: Class (RI,(0. X)) c= I

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I or x in Class (RI,(0. X)) )
assume A2: x in I ; :: thesis: x in Class (RI,(0. X))
then reconsider x = x as Element of I ;
A3: x \ (0. X) in I by A2, BCIALG_1:2;
x ` in I by A1;
then ( 0. X in {(0. X)} & [(0. X),x] in RI ) by A3, Def12, TARSKI:def 1;
hence x in Class (RI,(0. X)) by RELAT_1:def 13; :: thesis: verum

end;

thus Class (RI,(0. X)) c= I by Th38; :: thesis: verum

end;

assume A4: I = Class (RI,(0. X)) ; :: thesis: I is closed

now :: thesis: for x being Element of I holds x ` in I

let x be Element of I; :: thesis: x ` in I
ex y being object st
( [y,x] in RI & y in {(0. X)} ) by A4, RELAT_1:def 13;
then [(0. X),x] in RI by TARSKI:def 1;
hence x ` in I by Def12; :: thesis: verum

end;

hence I is closed ; :: thesis: verum