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


begin

:: 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 Element of NAT ;
func(x,y) to_power n ->  Element of X means :Def1: :: BCIALG_2:def 1
 ex f being Function of NAT, the carrier of X st
( it = f . n &amp; f . 0 = x &amp; ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) );
existence
 ex b1 being Element of X ex f being Function of NAT, the carrier of X st
( b1 = f . n &amp; f . 0 = x &amp; ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) )
proofend;
uniqueness
 for b1, b2 being Element of X st ex f being Function of NAT, the carrier of X st
( b1 = f . n &amp; f . 0 = x &amp; ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) &amp; ex f being Function of NAT, the carrier of X st
( b2 = f . n &amp; f . 0 = x &amp; ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) holds
b1 = b2
proofend;
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 Element of NAT
for b5 being Element of X holds
( b5 = (x,y) to_power n iff ex f being Function of NAT, the carrier of X st
( b5 = f . n &amp; f . 0 = x &amp; ( for j being Element of 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
proofend;

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
proofend;

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
proofend;

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

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

theorem Th6: :: BCIALG_2:6
for X being BCI-algebra
for n being Element of NAT holds ((0. X),(0. X)) to_power n = 0. X
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;
attra is positive  means :Def2: :: BCIALG_2:def 2
 0. X <= a;
attra is least  means :: BCIALG_2:def 3
 for x being Element of X holds a <= x;
attra is maximal  means :Def4: :: BCIALG_2:def 4
 for x being Element of X st a <= x holds
x = a;
attra is greatest  means :Def5: :: 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 Def4 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 Def5 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 )
proofend;

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

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
proofend;
end;

Lm3:  for X being BCI-algebra holds 0. X is minimal
proofend;

registration
let X be BCI-algebra;
cluster 0. X ->  minimal positive ;
coherence
 ( 0. X is positive &amp; 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 `) )
proofend;

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 ` )
proofend;

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 `) )
proofend;

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
proofend;

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
proofend;

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

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

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 ` )
proofend;

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

:: deftheorem Def6 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 empty Element of NAT st ((0. X),x) to_power k = 0. X );

definition
let X be BCI-algebra;
attrX 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 empty Element of NAT  means :Def8: :: BCIALG_2:def 8
( ((0. X),x) to_power it = 0. X &amp; ( for m being Element of NAT st ((0. X),x) to_power m = 0. X &amp; m <> 0 holds
it <= m ) );
existence
 ex b1 being non empty Element of NAT st
( ((0. X),x) to_power b1 = 0. X &amp; ( for m being Element of NAT st ((0. X),x) to_power m = 0. X &amp; m <> 0 holds
b1 <= m ) )
proofend;
uniqueness
 for b1, b2 being non empty Element of NAT st ((0. X),x) to_power b1 = 0. X &amp; ( for m being Element of NAT st ((0. X),x) to_power m = 0. X &amp; m <> 0 holds
b1 <= m ) &amp; ((0. X),x) to_power b2 = 0. X &amp; ( for m being Element of NAT st ((0. X),x) to_power m = 0. X &amp; m <> 0 holds
b2 <= m ) holds
b1 = b2
proofend;
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 empty Element of NAT holds
( b3 = ord x iff ( ((0. X),x) to_power b3 = 0. X &amp; ( for m being Element of NAT st ((0. X),x) to_power m = 0. X &amp; m <> 0 holds
b3 <= m ) ) );

registration
let X be BCI-algebra;
cluster 0. X ->  nilpotent ;
coherence
 0. X is nilpotent
proofend;
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 &amp; ord x = 1 ) )
proofend;

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 &amp; x is nilpotent ) )
proofend;

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

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

begin

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 &amp; [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 &amp; [u,v] in b1 holds
[(x \ u),(y \ v)] in b1
proofend;
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 &amp; [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
proofend;
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
proofend;
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 &amp; 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 &amp; y \ x in A ) )
proofend;
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 &amp; 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 &amp; b1 is symmetric &amp; b1 is transitive )
proofend;
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 )
proofend;
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 ) ) &amp; ( 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
proofend;
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
proofend;

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 &amp; R is L-congruence of X ) )
proofend;

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
proofend;

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
proofend;

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)) )
proofend;

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)) &amp; y \ x in Class (E,(0. X)) )
proofend;

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
proofend;

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

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 Element of 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
proofend;

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

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

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

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

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
proofend;

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
proofend;

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
proofend;

registration
let X be BCI-algebra;
let E be Congruence of X;
cluster Class E ->  non empty ;
coherence
 not Class E is empty
proofend;
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) &amp; 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) &amp; W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y))
proofend;
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) &amp; W2 = Class (E,y) holds
b1 . (W1,W2) = Class (E,(x \ y)) ) &amp; ( for W1, W2 being Element of Class E
for x, y being Element of X st W1 = Class (E,x) &amp; W2 = Class (E,y) holds
b2 . (W1,W2) = Class (E,(x \ y)) ) holds
b1 = b2
proofend;
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) &amp; 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;
funcX ./. 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;
clusterX ./. 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;
funcW1 \ 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
proofend;

registration
let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
clusterX ./. RI ->  strict being_B being_C being_I being_BCI-4 ;
coherence
 ( X ./. RI is strict &amp; X ./. RI is being_B &amp; X ./. RI is being_C &amp; X ./. RI is being_I &amp; 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
proofend;