let X be BCI-algebra; for I being Ideal of X
for RI being I-congruence of X,I holds RI is Congruence of X
let I be Ideal of X; for RI being I-congruence of X,I holds RI is Congruence of X
let RI be I-congruence of X,I; RI is Congruence of X
field RI = the carrier of X
by EQREL_1:9;
then A1:
RI is_transitive_in the carrier of X
by RELAT_2:def 16;
now for x, y, u, v being Element of X st [x,y] in RI & [u,v] in RI holds
[(x \ u),(y \ v)] in RIlet x,
y,
u,
v be
Element of
X;
( [x,y] in RI & [u,v] in RI implies [(x \ u),(y \ v)] in RI )assume that A2:
[x,y] in RI
and A3:
[u,v] in RI
;
[(x \ u),(y \ v)] in RI
((y \ u) \ (y \ v)) \ (v \ u) = 0. X
by BCIALG_1:1;
then A4:
((y \ u) \ (y \ v)) \ (v \ u) in I
by BCIALG_1:def 18;
v \ u in I
by A3, Def12;
then A5:
(y \ u) \ (y \ v) in I
by A4, BCIALG_1:def 18;
((y \ v) \ (y \ u)) \ (u \ v) = 0. X
by BCIALG_1:1;
then A6:
((y \ v) \ (y \ u)) \ (u \ v) in I
by BCIALG_1:def 18;
u \ v in I
by A3, Def12;
then
(y \ v) \ (y \ u) in I
by A6, BCIALG_1:def 18;
then A7:
[(y \ u),(y \ v)] in RI
by A5, Def12;
((x \ u) \ (y \ u)) \ (x \ y) = 0. X
by BCIALG_1:def 3;
then A8:
((x \ u) \ (y \ u)) \ (x \ y) in I
by BCIALG_1:def 18;
((y \ u) \ (x \ u)) \ (y \ x) = 0. X
by BCIALG_1:def 3;
then A9:
((y \ u) \ (x \ u)) \ (y \ x) in I
by BCIALG_1:def 18;
y \ x in I
by A2, Def12;
then A10:
(y \ u) \ (x \ u) in I
by A9, BCIALG_1:def 18;
x \ y in I
by A2, Def12;
then
(x \ u) \ (y \ u) in I
by A8, BCIALG_1:def 18;
then
[(x \ u),(y \ u)] in RI
by A10, Def12;
hence
[(x \ u),(y \ v)] in RI
by A1, A7, RELAT_2:def 8;
verum end;
hence
RI is Congruence of X
by Def9; verum