let X be BCI-algebra; :: thesis: 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; :: thesis: for RI being I-congruence of X,I holds RI is Congruence of X

let RI be I-congruence of X,I; :: thesis: 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;

for RI being I-congruence of X,I holds RI is Congruence of X

let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds RI is Congruence of X

let RI be I-congruence of X,I; :: thesis: 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 :: thesis: for x, y, u, v being Element of X st [x,y] in RI & [u,v] in RI holds

[(x \ u),(y \ v)] in RI

hence
RI is Congruence of X
by Def9; :: thesis: verum[(x \ u),(y \ v)] in RI

let x, y, u, v be Element of X; :: thesis: ( [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 ; :: thesis: [(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; :: thesis: verum

end;assume that

A2: [x,y] in RI and

A3: [u,v] in RI ; :: thesis: [(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; :: thesis: verum