let X be BCI-algebra; :: thesis: for I being Ideal of X
for RI being I-congruence of X,I holds Class RI,(0. X) c= I
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds Class RI,(0. X) c= I
let RI be I-congruence of X,I; :: thesis: Class RI,(0. X) c= I
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Class RI,(0. X) or x in I )
assume A1: x in Class RI,(0. X) ; :: thesis: x in I
then consider y being set such that
A2: ( [y,x] in RI & y in {(0. X)} ) by RELAT_1:def 13;
reconsider y = y as Element of X by A2, TARSKI:def 1;
reconsider x = x as Element of X by A1;
y = 0. X by A2, TARSKI:def 1;
then x \ (0. X) in I by A2, Def12;
hence x in I by BCIALG_1:2; :: thesis: verum