:: Congruences and Quotient Algebras of {BCI}-algebras
:: by Yuzhong Ding and Zhiyong Pang
::
:: Received August 28, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


:: x*y to_power n = x*y|^n
:: n=0: it=x; n=1:it =x*y; n=2:it=(x*y)*y...
definition
let X be BCI-algebra;
let x, y be Element of X;
let n be Nat;
func (x,y) to_power n -> Element of X means :Def1: :: BCIALG_2:def 1
 ex f being sequence of the carrier of X st
( it = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) );
existence
ex b1 being Element of X ex f being sequence of the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) )
proof end;
uniqueness
for b1, b2 being Element of X st ex f being sequence of the carrier of X st
( b1 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being sequence of the carrier of X st
( b2 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines to_power BCIALG_2:def 1 :
for X being BCI-algebra
for x, y being Element of X
for n being Nat
for b5 being Element of X holds
( b5 = (x,y) to_power n iff ex f being sequence of the carrier of X st
( b5 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) );

theorem Th1: :: BCIALG_2:1
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 0 = x
proof end;

theorem Th2: :: BCIALG_2:2
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 1 = x \ y
proof end;

theorem :: BCIALG_2:3
for X being BCI-algebra
for x, y being Element of X holds (x,y) to_power 2 = (x \ y) \ y
proof end;

theorem Th4: :: BCIALG_2:4
for X being BCI-algebra
for x, y being Element of X
for n being Nat holds (x,y) to_power (n + 1) = ((x,y) to_power n) \ y
proof end;

theorem Th5: :: BCIALG_2:5
for X being BCI-algebra
for x being Element of X
for n being Nat holds (x,(0. X)) to_power (n + 1) = x
proof end;

theorem Th6: :: BCIALG_2:6
for X being BCI-algebra
for n being Nat holds ((0. X),(0. X)) to_power n = 0. X
proof end;

theorem Th7: :: BCIALG_2:7
for X being BCI-algebra
for x, y, z being Element of X
for n being Nat holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
proof end;

theorem :: BCIALG_2:8
for X being BCI-algebra
for x, y being Element of X
for n being Nat holds (x,(x \ (x \ y))) to_power n = (x,y) to_power n
proof end;

theorem Th9: :: BCIALG_2:9
for X being BCI-algebra
for x being Element of X
for n being Nat holds (((0. X),x) to_power n) ` = ((0. X),(x `)) to_power n
proof end;

theorem Th10: :: BCIALG_2:10
for X being BCI-algebra
for x, y being Element of X
for n, m being Nat holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)
proof end;

theorem :: BCIALG_2:11
for X being BCI-algebra
for x, y, z being Element of X
for n, m being Nat holds (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n
proof end;

theorem Th12: :: BCIALG_2:12
for X being BCI-algebra
for x being Element of X
for n being Nat holds ((((0. X),x) to_power n) `) ` = ((0. X),x) to_power n
proof end;

theorem Th13: :: BCIALG_2:13
for X being BCI-algebra
for x being Element of X
for n, m being Nat holds ((0. X),x) to_power (n + m) = (((0. X),x) to_power n) \ ((((0. X),x) to_power m) `)
proof end;

theorem :: BCIALG_2:14
for X being BCI-algebra
for x being Element of X
for n, m being Nat holds (((0. X),x) to_power (m + n)) ` = ((((0. X),x) to_power m) `) \ (((0. X),x) to_power n)
proof end;

theorem :: BCIALG_2:15
for X being BCI-algebra
for x being Element of X
for n, m being Nat holds (((0. X),(((0. X),x) to_power m)) to_power n) ` = ((0. X),x) to_power (m * n)
proof end;

theorem :: BCIALG_2:16
for X being BCI-algebra
for x being Element of X
for n, m being Nat st ((0. X),x) to_power m = 0. X holds
((0. X),x) to_power (m * n) = 0. X
proof end;

theorem :: BCIALG_2:17
for X being BCI-algebra
for x, y being Element of X
for n being Nat st x \ y = x holds
(x,y) to_power n = x
proof end;

theorem :: BCIALG_2:18
for X being BCI-algebra
for x, y being Element of X
for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)
proof end;

::P20-P22
theorem :: BCIALG_2:19
for X being BCI-algebra
for x, y, z being Element of X
for n being Nat st x <= y holds
(x,z) to_power n <= (y,z) to_power n
proof end;

theorem :: BCIALG_2:20
for X being BCI-algebra
for x, y, z being Element of X
for n being Nat st x <= y holds
(z,y) to_power n <= (z,x) to_power n
proof end;

theorem :: BCIALG_2:21
for X being BCI-algebra
for x, y, z being Element of X
for n being Nat holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
proof end;

theorem :: BCIALG_2:22
for X being BCI-algebra
for x, y being Element of X
for n being Nat holds (((x,(x \ y)) to_power n),(y \ x)) to_power n <= x
proof end;

notation
let X be BCI-algebra;
let a be Element of X;
synonym minimal a for atom ;
end;

::P17 proposition 1.1.10
definition
let X be BCI-algebra;
let a be Element of X;
attr a is positive means :Def2: :: BCIALG_2:def 2
 0. X <= a;
attr a is least means :: BCIALG_2:def 3
 for x being Element of X holds a <= x;
attr a is maximal means :: BCIALG_2:def 4
 for x being Element of X st a <= x holds
x = a;
attr a is greatest means :: BCIALG_2:def 5
 for x being Element of X holds x <= a;
end;

:: deftheorem Def2 defines positive BCIALG_2:def 2 :
for X being BCI-algebra
for a being Element of X holds
( a is positive iff 0. X <= a );

:: deftheorem defines least BCIALG_2:def 3 :
for X being BCI-algebra
for a being Element of X holds
( a is least iff for x being Element of X holds a <= x );

:: deftheorem defines maximal BCIALG_2:def 4 :
for X being BCI-algebra
for a being Element of X holds
( a is maximal iff for x being Element of X st a <= x holds
x = a );

:: deftheorem defines greatest BCIALG_2:def 5 :
for X being BCI-algebra
for a being Element of X holds
( a is greatest iff for x being Element of X holds x <= a );

Lm1: for X being BCI-algebra
for a being Element of X holds
( a is minimal iff for x being Element of X st x <= a holds
x = a )
by BCIALG_1:def 11;

Lm2: for X being BCI-algebra holds 0. X is positive
proof end;

registration
let X be BCI-algebra;
cluster positive for Element of the carrier of X;
existence
ex b1 being Element of X st b1 is positive
proof end;
end;

Lm3: for X being BCI-algebra holds 0. X is minimal
by BCIALG_1:2;

registration
let X be BCI-algebra;
cluster 0. X -> minimal positive ;
coherence
( 0. X is positive & 0. X is minimal ) by Lm2, Lm3;
end;

theorem :: BCIALG_2:23
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff for x being Element of X holds a \ x = (x `) \ (a `) )
proof end;

theorem :: BCIALG_2:24
for X being BCI-algebra
for x being Element of X holds
( x ` is minimal iff for y being Element of X st y <= x holds
x ` = y ` )
proof end;

theorem :: BCIALG_2:25
for X being BCI-algebra
for x being Element of X holds
( x ` is minimal iff for y, z being Element of X holds (((x \ z) \ (y \ z)) `) ` = (y `) \ (x `) )
proof end;

theorem :: BCIALG_2:26
for X being BCI-algebra st 0. X is maximal holds
for a being Element of X holds a is minimal
proof end;

theorem :: BCIALG_2:27
for X being BCI-algebra st ex x being Element of X st x is greatest holds
for a being Element of X holds a is positive
proof end;

theorem Th28: :: BCIALG_2:28
for X being BCI-algebra
for x being Element of X holds x \ ((x `) `) is positive Element of X
proof end;

theorem :: BCIALG_2:29
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff (a `) ` = a )
proof end;

theorem Th30: :: BCIALG_2:30
for X being BCI-algebra
for a being Element of X holds
( a is minimal iff ex x being Element of X st a = x ` )
proof end;

:: p38
definition
let X be BCI-algebra;
let x be Element of X;
attr x is nilpotent means :: BCIALG_2:def 6
 ex k being non zero Nat st ((0. X),x) to_power k = 0. X;
end;

:: deftheorem defines nilpotent BCIALG_2:def 6 :
for X being BCI-algebra
for x being Element of X holds
( x is nilpotent iff ex k being non zero Nat st ((0. X),x) to_power k = 0. X );

definition
let X be BCI-algebra;
attr X is nilpotent means :: BCIALG_2:def 7
 for x being Element of X holds x is nilpotent ;
end;

:: deftheorem defines nilpotent BCIALG_2:def 7 :
for X being BCI-algebra holds
( X is nilpotent iff for x being Element of X holds x is nilpotent );

definition
let X be BCI-algebra;
let x be Element of X;
assume A1: x is nilpotent ;
func ord x -> non zero Nat means :Def8: :: BCIALG_2:def 8
( ((0. X),x) to_power it = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
it <= m ) );
existence
ex b1 being non zero Nat st
( ((0. X),x) to_power b1 = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b1 <= m ) )
proof end;
uniqueness
for b1, b2 being non zero Nat st ((0. X),x) to_power b1 = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b1 <= m ) & ((0. X),x) to_power b2 = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b2 <= m ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem Def8 defines ord BCIALG_2:def 8 :
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
for b3 being non zero Nat holds
( b3 = ord x iff ( ((0. X),x) to_power b3 = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b3 <= m ) ) );

registration
let X be BCI-algebra;
cluster 0. X -> nilpotent ;
coherence
0. X is nilpotent
proof end;
end;

theorem :: BCIALG_2:31
for X being BCI-algebra
for x being Element of X holds
( x is positive Element of X iff ( x is nilpotent & ord x = 1 ) )
proof end;

theorem :: BCIALG_2:32
for X being BCI-algebra holds
( X is BCK-algebra iff for x being Element of X holds
( ord x = 1 & x is nilpotent ) )
proof end;

theorem :: BCIALG_2:33
for X being BCI-algebra
for x being Element of X
for n being Nat holds ((0. X),(x `)) to_power n is minimal
proof end;

theorem :: BCIALG_2:34
for X being BCI-algebra
for x being Element of X st x is nilpotent holds
ord x = ord (x `)
proof end;

definition
let X be BCI-algebra;
mode Congruence of X -> Equivalence_Relation of X means :Def9: :: BCIALG_2:def 9
 for x, y, u, v being Element of X st [x,y] in it & [u,v] in it holds
[(x \ u),(y \ v)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y, u, v being Element of X st [x,y] in b1 & [u,v] in b1 holds
[(x \ u),(y \ v)] in b1
proof end;
end;

:: deftheorem Def9 defines Congruence BCIALG_2:def 9 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is Congruence of X iff for x, y, u, v being Element of X st [x,y] in b2 & [u,v] in b2 holds
[(x \ u),(y \ v)] in b2 );

:: Left Congruence
definition
let X be BCI-algebra;
mode L-congruence of X -> Equivalence_Relation of X means :Def10: :: BCIALG_2:def 10
 for x, y being Element of X st [x,y] in it holds
for u being Element of X holds [(u \ x),(u \ y)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(u \ x),(u \ y)] in b1
proof end;
end;

:: deftheorem Def10 defines L-congruence BCIALG_2:def 10 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is L-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(u \ x),(u \ y)] in b2 );

:: Right Congruence
definition
let X be BCI-algebra;
mode R-congruence of X -> Equivalence_Relation of X means :Def11: :: BCIALG_2:def 11
 for x, y being Element of X st [x,y] in it holds
for u being Element of X holds [(x \ u),(y \ u)] in it;
existence
ex b1 being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b1 holds
for u being Element of X holds [(x \ u),(y \ u)] in b1
proof end;
end;

:: deftheorem Def11 defines R-congruence BCIALG_2:def 11 :
for X being BCI-algebra
for b2 being Equivalence_Relation of X holds
( b2 is R-congruence of X iff for x, y being Element of X st [x,y] in b2 holds
for u being Element of X holds [(x \ u),(y \ u)] in b2 );

::Ideal Congruence
definition
let X be BCI-algebra;
let A be Ideal of X;
mode I-congruence of X,A -> Relation of X means :Def12: :: BCIALG_2:def 12
 for x, y being Element of X holds
( [x,y] in it iff ( x \ y in A & y \ x in A ) );
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( [x,y] in b1 iff ( x \ y in A & y \ x in A ) )
proof end;
end;

:: deftheorem Def12 defines I-congruence BCIALG_2:def 12 :
for X being BCI-algebra
for A being Ideal of X
for b3 being Relation of X holds
( b3 is I-congruence of X,A iff for x, y being Element of X holds
( [x,y] in b3 iff ( x \ y in A & y \ x in A ) ) );

registration
let X be BCI-algebra;
let A be Ideal of X;
cluster -> total symmetric transitive for I-congruence of X,A;
coherence
for b1 being I-congruence of X,A holds
( b1 is total & b1 is symmetric & b1 is transitive )
proof end;
end;

definition
let X be BCI-algebra;
func IConSet X -> set means :Def13: :: BCIALG_2:def 13
 for A1 being set holds
( A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I );
existence
ex b1 being set st
for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I )
proof end;
uniqueness
for b1, b2 being set st ( for A1 being set holds
( A1 in b1 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :
for X being BCI-algebra
for b2 being set holds
( b2 = IConSet X iff for A1 being set holds
( A1 in b2 iff ex I being Ideal of X st A1 is I-congruence of X,I ) );

definition
let X be BCI-algebra;
func ConSet X -> set equals :: BCIALG_2:def 14
 { R where R is Congruence of X : verum } ;
coherence
{ R where R is Congruence of X : verum } is set ;
func LConSet X -> set equals :: BCIALG_2:def 15
 { R where R is L-congruence of X : verum } ;
coherence
{ R where R is L-congruence of X : verum } is set ;
func RConSet X -> set equals :: BCIALG_2:def 16
 { R where R is R-congruence of X : verum } ;
coherence
{ R where R is R-congruence of X : verum } is set ;
end;

:: deftheorem defines ConSet BCIALG_2:def 14 :
for X being BCI-algebra holds ConSet X = { R where R is Congruence of X : verum } ;

:: deftheorem defines LConSet BCIALG_2:def 15 :
for X being BCI-algebra holds LConSet X = { R where R is L-congruence of X : verum } ;

:: deftheorem defines RConSet BCIALG_2:def 16 :
for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;

:: huang-P58:P1.5.1
theorem :: BCIALG_2:35
for X being BCI-algebra
for E being Congruence of X holds Class (E,(0. X)) is closed Ideal of X
proof end;

theorem Th36: :: BCIALG_2:36
for X being BCI-algebra
for R being Equivalence_Relation of X holds
( R is Congruence of X iff ( R is R-congruence of X & R is L-congruence of X ) )
proof end;

theorem Th37: :: BCIALG_2:37
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds RI is Congruence of X
proof end;

definition
let X be BCI-algebra;
let I be Ideal of X;
:: original: I-congruence
redefine mode I-congruence of X,I -> Congruence of X;
coherence
for b1 being I-congruence of X,I holds b1 is Congruence of X by Th37;
end;

theorem Th38: :: BCIALG_2:38
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds Class (RI,(0. X)) c= I
proof end;

theorem :: BCIALG_2:39
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds
( I is closed iff I = Class (RI,(0. X)) )
proof end;

theorem Th40: :: BCIALG_2:40
for X being BCI-algebra
for x, y being Element of X
for E being Congruence of X st [x,y] in E holds
( x \ y in Class (E,(0. X)) & y \ x in Class (E,(0. X)) )
proof end;

theorem :: BCIALG_2:41
for X being BCI-algebra
for A, I being Ideal of X
for IA being I-congruence of X,A
for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II
proof end;

theorem Th42: :: BCIALG_2:42
for X being BCI-algebra
for x, y, u being Element of X
for k being Nat
for E being Congruence of X st [x,y] in E & u in Class (E,(0. X)) holds
[x,((y,u) to_power k)] in E
proof end;

theorem :: BCIALG_2:43
for X being BCI-algebra st ( 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 ) holds
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
proof end;

theorem :: BCIALG_2:44
for X being BCI-algebra holds IConSet X c= ConSet X
proof end;

theorem Th45: :: BCIALG_2:45
for X being BCI-algebra holds ConSet X c= LConSet X
proof end;

theorem Th46: :: BCIALG_2:46
for X being BCI-algebra holds ConSet X c= RConSet X
proof end;

theorem :: BCIALG_2:47
for X being BCI-algebra holds ConSet X = (LConSet X) /\ (RConSet X)
proof end;

theorem :: BCIALG_2:48
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
proof end;

theorem :: BCIALG_2:49
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for RC being R-congruence of X holds RC is I-congruence of X,I ) holds
E = RI
proof end;

theorem :: BCIALG_2:50
for X being BCI-algebra
for LC being L-congruence of X holds Class (LC,(0. X)) is closed Ideal of X
proof end;

registration
let X be BCI-algebra;
let E be Congruence of X;
cluster Class E -> non empty ;
coherence
not Class E is empty
proof end;
end;

definition
let X be BCI-algebra;
let E be Congruence of X;
func EqClaOp E -> BinOp of (Class E) means :Def17: :: BCIALG_2:def 17
 for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
it . (W1,W2) = Class (E,(x \ y));
existence
ex b1 being BinOp of (Class E) st
for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y))
proof end;
uniqueness
for b1, b2 being BinOp of (Class E) st ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y)) ) & ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b2 . (W1,W2) = Class (E,(x \ y)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines EqClaOp BCIALG_2:def 17 :
for X being BCI-algebra
for E being Congruence of X
for b3 being BinOp of (Class E) holds
( b3 = EqClaOp E iff for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
b3 . (W1,W2) = Class (E,(x \ y)) );

definition
let X be BCI-algebra;
let E be Congruence of X;
func zeroEqC E -> Element of Class E equals :: BCIALG_2:def 18
 Class (E,(0. X));
coherence
Class (E,(0. X)) is Element of Class E by EQREL_1:def 3;
end;

:: deftheorem defines zeroEqC BCIALG_2:def 18 :
for X being BCI-algebra
for E being Congruence of X holds zeroEqC E = Class (E,(0. X));

::Quotient Algebras
definition
let X be BCI-algebra;
let E be Congruence of X;
func X ./. E -> BCIStr_0 equals :: BCIALG_2:def 19
 BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);
coherence
BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #) is BCIStr_0 ;
end;

:: deftheorem defines ./. BCIALG_2:def 19 :
for X being BCI-algebra
for E being Congruence of X holds X ./. E = BCIStr_0(# (Class E),(EqClaOp E),(zeroEqC E) #);

registration
let X be BCI-algebra;
let E be Congruence of X;
cluster X ./. E -> non empty ;
coherence
not X ./. E is empty ;
end;

definition
let X be BCI-algebra;
let E be Congruence of X;
let W1, W2 be Element of Class E;
func W1 \ W2 -> Element of Class E equals :: BCIALG_2:def 20
(EqClaOp E) . (W1,W2);
coherence
(EqClaOp E) . (W1,W2) is Element of Class E ;
end;

:: deftheorem defines \ BCIALG_2:def 20 :
for X being BCI-algebra
for E being Congruence of X
for W1, W2 being Element of Class E holds W1 \ W2 = (EqClaOp E) . (W1,W2);

theorem Th51: :: BCIALG_2:51
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
proof end;

registration
let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
cluster X ./. RI -> strict being_B being_C being_I being_BCI-4 ;
coherence
( X ./. RI is strict & X ./. RI is being_B & X ./. RI is being_C & X ./. RI is being_I & X ./. RI is being_BCI-4 ) by Th51;
end;

theorem :: BCIALG_2:52
for X being BCI-algebra
for I being Ideal of X st I = BCK-part X holds
for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra
proof end;