:: 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 b₁ being Element of X ex f being sequence of the carrier of X st
( b₁ = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) )

proof end;

uniqueness
for b₁, b₂ being Element of X st ex f being sequence of the carrier of X st
( b₁ = 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
( b₂ = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) holds
b₁ = b₂

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 b₅ being Element of X holds
( b₅ = (x,y) to_power n iff ex f being sequence of the carrier of X st
( b₅ = 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 b₁ being Element of X st b₁ 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 b₁ being non zero Nat st
( ((0. X),x) to_power b₁ = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b₁ <= m ) )

proof end;

uniqueness
for b₁, b₂ being non zero Nat st ((0. X),x) to_power b₁ = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b₁ <= m ) & ((0. X),x) to_power b₂ = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b₂ <= m ) holds
b₁ = b₂

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 b₃ being non zero Nat holds
( b₃ = ord x iff ( ((0. X),x) to_power b₃ = 0. X & ( for m being Nat st ((0. X),x) to_power m = 0. X & m <> 0 holds
b₃ <= 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 b₁ being Equivalence_Relation of X st
for x, y, u, v being Element of X st [x,y] in b₁ & [u,v] in b₁ holds
[(x \ u),(y \ v)] in b₁

proof end;

end;

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

:: 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 b₁ being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b₁ holds
for u being Element of X holds [(u \ x),(u \ y)] in b₁

proof end;

end;

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

:: 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 b₁ being Equivalence_Relation of X st
for x, y being Element of X st [x,y] in b₁ holds
for u being Element of X holds [(x \ u),(y \ u)] in b₁

proof end;

end;

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

::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 b₁ being Relation of X st
for x, y being Element of X holds
( [x,y] in b₁ 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 b₃ being Relation of X holds
( b₃ is I-congruence of X,A iff for x, y being Element of X holds
( [x,y] in b₃ 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 b₁ being I-congruence of X,A holds
( b₁ is total & b₁ is symmetric & b₁ 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 b₁ being set st
for A1 being set holds
( A1 in b₁ iff ex I being Ideal of X st A1 is I-congruence of X,I )

proof end;

uniqueness
for b₁, b₂ being set st ( for A1 being set holds
( A1 in b₁ iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) & ( for A1 being set holds
( A1 in b₂ iff ex I being Ideal of X st A1 is I-congruence of X,I ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines IConSet BCIALG_2:def 13 :
for X being BCI-algebra
for b₂ being set holds
( b₂ = IConSet X iff for A1 being set holds
( A1 in b₂ 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 b₁ being I-congruence of X,I holds b₁ 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 b₁ 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
b₁ . (W1,W2) = Class (E,(x \ y))

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (W1,W2) = Class (E,(x \ y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines EqClaOp BCIALG_2:def 17 :
for X being BCI-algebra
for E being Congruence of X
for b₃ being BinOp of (Class E) holds
( b₃ = 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
b₃ . (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;