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 object ; :: 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 object such that
A2: [y,x] in RI and
A3: y in {(0. X)} by RELAT_1:def 13;
reconsider x = x as Element of X by A1;
reconsider y = y as Element of X by A3, TARSKI:def 1;
y = 0. X by A3, TARSKI:def 1;
then x \ (0. X) in I by A2, Def12;
hence x in I by BCIALG_1:2; :: thesis: verum