let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ) implies for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I )
assume A1: for X being BCI-algebra
for x, y being Element of X ex i, j, m, n being Nat st (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n ; :: thesis: for E being Congruence of X
for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let E be Congruence of X; :: thesis: for I being Ideal of X st I = Class (E,(0. X)) holds
E is I-congruence of X,I
let I be Ideal of X; :: thesis: ( I = Class (E,(0. X)) implies E is I-congruence of X,I )
assume A2: I = Class (E,(0. X)) ; :: thesis: E is I-congruence of X,I

now :: thesis: for x, y being Element of X holds
( [x,y] in E iff ( x \ y in I & y \ x in I ) )

let x, y be Element of X; :: thesis: ( [x,y] in E iff ( x \ y in I & y \ x in I ) )
( x \ y in I & y \ x in I implies [x,y] in E )

proof

assume that
A3: x \ y in I and
A4: y \ x in I ; :: thesis: [x,y] in E
ex z being object st
( [z,(y \ x)] in E & z in {(0. X)} ) by A2, A4, RELAT_1:def 13;
then A5: [(0. X),(y \ x)] in E by TARSKI:def 1;
ex z being object st
( [z,(x \ y)] in E & z in {(0. X)} ) by A2, A3, RELAT_1:def 13;
then A6: [(0. X),(x \ y)] in E by TARSKI:def 1;
consider i, j, m, n being Nat such that
A7: (((x,(x \ y)) to_power i),(y \ x)) to_power j = (((y,(y \ x)) to_power m),(x \ y)) to_power n by A1;
A8: field E = the carrier of X by EQREL_1:9;
A9: E is_reflexive_in field E by RELAT_2:def 9;
then [x,x] in E by A8, RELAT_2:def 1;
then A10: [x,((x,(x \ y)) to_power i)] in E by A2, A3, Th42;
A11: [x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E

proof

defpred S₁[ Nat] means [x,((((x,(x \ y)) to_power i),(y \ x)) to_power $1)] in E;
A12: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume [x,((((x,(x \ y)) to_power i),(y \ x)) to_power k)] in E ; :: thesis: S₁[k + 1]
then [(x \ (0. X)),(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by A5, Def9;
then [x,(((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by BCIALG_1:2;
hence S₁[k + 1] by Th4; :: thesis: verum

end;

A13: S₁[ 0 ] by A10, Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A12);
hence [x,((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E ; :: thesis: verum

end;

[y,y] in E by A8, A9, RELAT_2:def 1;
then A14: [y,((y,(y \ x)) to_power m)] in E by A2, A4, Th42;
A15: [y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E

proof

defpred S₁[ Nat] means [y,((((y,(y \ x)) to_power m),(x \ y)) to_power $1)] in E;
A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume [y,((((y,(y \ x)) to_power m),(x \ y)) to_power k)] in E ; :: thesis: S₁[k + 1]
then [(y \ (0. X)),(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by A6, Def9;
then [y,(((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by BCIALG_1:2;
hence S₁[k + 1] by Th4; :: thesis: verum

end;

A17: S₁[ 0 ] by A14, Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A16);
hence [y,((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E ; :: thesis: verum

end;

E is_symmetric_in field E by RELAT_2:def 11;
then ( E is_transitive_in field E & [((((x,(x \ y)) to_power i),(y \ x)) to_power j),y] in E ) by A7, A8, A15, RELAT_2:def 3, RELAT_2:def 16;
hence [x,y] in E by A8, A11, RELAT_2:def 8; :: thesis: verum

end;

hence ( [x,y] in E iff ( x \ y in I & y \ x in I ) ) by A2, Th40; :: thesis: verum

end;

hence E is I-congruence of X,I by Def12; :: thesis: verum