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

environ

 vocabularies BCIALG_2, FUNCT_1, ASYMPT_0, RLVECT_1, FUNCOP_1, GROUP_4,
      BINOP_1, POWER, BCIALG_1, RELAT_1, BOOLE, EQREL_1, ALG_1, GROUP_6,
      FILTER_2, PRE_TOPC, RELAT_2, GROUP_1, WAYBEL15, SUBSET_1, CHORD,
      PARTFUN1, ARYTM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      NAT_1, FUNCT_2, XXREAL_0, FUNCOP_1, BINOP_1, STRUCT_0, BCIALG_1, RELAT_2,
      PARTFUN1, EQREL_1, ALG_1;
 constructors BCIALG_1, BINOP_1, XXREAL_0, NAT_1, VECTSP_1, BINARITH, EQREL_1;
 registrations BCIALG_1, SUBSET_1, NAT_1, RELSET_1, STRUCT_0, PARTFUN1,
      ORDINAL1, XREAL_0, XBOOLE_0;
 requirements NUMERALS, ARITHM, SUBSET, BOOLE;
 definitions XBOOLE_0, TARSKI, STRUCT_0, BCIALG_1, RELAT_1;
 theorems BCIALG_1, FUNCOP_1, NAT_1, XREAL_1, REAL_1, TARSKI, XBOOLE_0,
      RELAT_2, RELAT_1, XXREAL_0, ORDERS_1, XBOOLE_1, BINOP_1, EQREL_1,
      RELSET_1, ZFMISC_1;
 schemes FUNCT_2, NAT_1, RELSET_1, XBOOLE_0, BINOP_1;

begin :: Basic Properties of The Element P16-P19

reserve X,Y for BCI-algebra;
reserve A,I,I1 for Ideal of X;
reserve a,x,y,z,u,v,h for Element of X;
reserve f,f',g for Function of NAT, the carrier of X;
reserve j,i,k,n,m for Element of NAT;

::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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,x,y;
  let n be Element of NAT;
  func (x,y) to_power n -> Element of X means
  :Def1:
  ex f st it = f.n & f.0 = x &
  for j being Element of NAT st j<n holds f.(j+1) = f.j\y;
  existence
  proof

defpred P[set] means for x,y being Element of X,n being Element of NAT st n=$1
    ex u being Element of X st ex f being Function of NAT, the carrier of X st
    u = f.n & f.0 = x &for j being Element of NAT st j<n holds f.(j+1) = f.j\y;
A1: P[0]
    proof
      now
        let x,y be Element of X,n be Element of NAT;
        assume
A2:     n = 0;

reconsider f = NAT-->x as Function of NAT, the carrier of X;
        take u = f.n;
        take f' = f;
        thus u = f'.n & f'.0 = x by FUNCOP_1:13;

thus for j being Element of NAT st j<n holds f'.(j+1) = f'.j\y by A2,NAT_1:3;
      end;
      hence thesis;
    end;
A3: for n be Element of NAT st P[n] holds P[n+1]
    proof
      now
        let n be Element of NAT;
        assume
A4:     for x,y,k st k=n ex u st ex f st u = f.k & f.0 = x &
        for j st j<k holds f.(j+1) = f.j\y;
        let x,y,k;
        assume k = n + 1;
        consider u,f such that u = f.n and
A5:     f.0= x and
A6:     for j st j<n holds f.(j+1) = f.j\y by A4;
A7:     n <n+1 by NAT_1:13;
        defpred P[set,set] means for j st $1=j
        holds (j<n + 1 implies $2 = f.$1) &(n+1<=j implies $2=f.n\y);
A8:     for k being Element of NAT ex v being Element of X st P[k,v]
        proof
          let k be Element of NAT;
          reconsider i = k as Element of NAT;
A9:       now
            assume
A10:        i < n + 1;
            take v = f.k;
            let j such that
A11:        k = j;
            thus j < n + 1 implies v = f.k;
            thus n + 1 <= j implies v = f.n \ y by A10,A11;
          end;
          now
            assume
A12:        n + 1 <= i;
            take v = f.n \ y;
            let j;
            assume k = j;
            hence j < n + 1 implies v = f.k by A12;
            assume n + 1 <= j;
            thus v = f.n \ y;
          end;
          hence thesis by A9;
        end;
        consider f' being Function of NAT, the carrier of X such that
A13:    for k being Element of NAT holds P[k,f'.k] from FUNCT_2:sch 3(A8);
        take z = f'.(n + 1);
        take f'' = f';
        thus z = f''.(n+1);
        0<n+1 by NAT_1:5;
        hence f''.0 = x by A5,A13;
        let j;
        assume that
A14:    j < n+1;
A15:    now
          assume
A16:      j < n;
          then f.(j + 1) = f.j \ y & j < n + 1 by A6,NAT_1:13;
          then f.(j + 1) = f'.j \ y & j + 1 < n + 1 by A13,A16,XREAL_1:8;
          hence f''.(j + 1) = f''.j \ y by A13;
        end;
A17:    now
          assume
A18:      j = n;
          then f''.(j + 1) = f.j \ y by A13;
          hence f''.(j + 1) = f''.j \ y by A7,A13,A18;
        end;
        j <= n by A14,NAT_1:13;
        hence f''.(j + 1) = f''.j \ y by A15,A17,REAL_1:def 5;
      end;
      hence thesis;
    end;
    for n holds P[n] from NAT_1:sch 1(A1,A3);
    then consider u such that
A19: ex f st u = f.n & f.0 = x & for j st j < n holds f.(j + 1) = f.j \ y;
    thus thesis by A19;
  end;
  uniqueness
  proof
    let v1,v2 be Element of X;
    given f such that
A20: v1 = f.n and
A21: f.0 = x and
A22: for j st j < n holds f.(j + 1) = f.j \ y;
    given f' such that
A23: v2 = f'.n and
A24: f'.0 = x and
A25: for j st j < n holds f'.(j + 1) = f'.j \ y;
    defpred P[Nat] means $1 <= n implies f.$1 = f'.$1;
A26: P[0] by A21,A24;
A27: for k st P[k] holds P[k+1]
    proof
      now
        let k;
        assume
A28:    k <= n implies f.k = f'.k;
        assume k + 1 <= n;
        then k < n by NAT_1:13;
        then f.(k + 1) = f.k \y & f'.(k + 1) = f'.k \ y & k <= n by A22,A25;
        hence f.(k + 1) = f'.(k + 1) by A28;
      end;
      hence thesis;
    end;
    for k holds P[k] from NAT_1:sch 1(A26,A27);
    hence v1 = v2 by A20,A23;
  end;
end;

theorem Th1:
  (x,y) to_power 0 = x
proof
  ex f st (x,y) to_power 0 = f.0 & f.0 = x &
  for j st j < 0 holds f.(j + 1) = f.j \ y by Def1;
  hence thesis;
end;

theorem Th2:
  (x,y) to_power 1 = x\y
proof
  consider f such that
A1: (x,y) to_power 1 = f.1 & f.0 = x &
  for j st j < 1 holds f.(j + 1) = f.j \ y by Def1;
  f.(0+1) = x\y by A1,NAT_1:3;
  hence thesis by A1;
end;

theorem
  (x,y) to_power 2 = x\y\y
proof
  consider f such that
A1: (x,y) to_power 2 = f.2 & f.0 = x &
  for j st j < 2 holds f.(j + 1) = f.j \ y by Def1;
  1<1+1 by NAT_1:13;
  then f.(1+1) = f.(0+1) \y by A1;
  hence thesis by A1,NAT_1:3;
end;

theorem Th4:
  (x,y) to_power (n+1) = (x,y) to_power n \ y
proof
  consider f such that
A1: (x,y) to_power (n+1) = f.(n+1) & f.0 = x &
  for j st j < n+1 holds f.(j + 1) = f.j \ y by Def1;
  consider g such that
A2: (x,y) to_power n = g.n & g.0 = x &
  for j st j < n holds g.(j + 1) = g.j \ y by Def1;
  defpred P[set] means for m holds m=$1 & m <= n implies f.m=g.m;
A3: P[0] by A1,A2;
A4: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A5:   for m st m=k & m<=n holds f.m=g.m;
      let m;
      assume
A6:   m=k+1 & m<=n;
A7:   k<n+1 & k<n & k<=n
      proof
        k +1 <= n+1 by A6,NAT_1:13;
        hence k<n+1 by NAT_1:13;
        thus k< n &k<=n by A6,NAT_1:13;
      end;
      then f.(k + 1) = f.k \y & g.(k + 1) = g.k \y by A1,A2;
      hence f.m=g.m by A5,A6,A7;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A3,A4);
  then
A8: f.n = g.n;
  n<n+1 by NAT_1:3,XREAL_1:31;
  hence thesis by A1,A2,A8;
end;

theorem Th5:
  (x,0.X) to_power (n+1) = x
proof
  defpred P[set] means
  for m holds m=$1 & m<= n implies (x,0.X) to_power (m+1) = x;
  now (x,0.X) to_power (0+1) = x \ 0.X by Th2;
    hence (x,0.X) to_power (0+1) = x by BCIALG_1:2;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m st m=k & m<= n holds (x,0.X) to_power (m+1) = x;
      let m;
      assume
A4:   m=k+1 & m<=n;
      then (x,0.X) to_power (m+1)=((x,0.X) to_power (k+1))\0.X by Th4;
      then
A5:   (x,0.X) to_power (m+1)=(x,0.X) to_power (k+1) by BCIALG_1:2;
      k<=n by A4,NAT_1:13;
      hence (x,0.X) to_power (m+1)= x by A3,A5;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th6:
  (0.X,0.X) to_power n=0.X
proof
  defpred P[set] means
  for m holds m=$1 & m<= n implies (0.X,0.X) to_power m = 0.X;
A1: P[0] by Th1;
A2: for k st P[k] holds P[k+1] by Th5;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th7:
  (x,y) to_power n\z = (x\z,y) to_power n
proof
  defpred P[set] means for m holds
  m=$1 & m<= n implies (x,y) to_power m\z = (x\z,y) to_power m;
  now (x,y) to_power 0\z = x\z by Th1;
    hence (x,y) to_power 0\z = (x\z,y) to_power 0 by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m st m=k & m<= n holds (x,y) to_power m\z = (x\z,y) to_power m;
      let m;
      assume
A4:   m=k+1 & m<=n;
      then (x,y) to_power m\z=((x,y) to_power k\y)\z by Th4;
      then
A5:   (x,y) to_power m\z=((x,y) to_power k\z)\y by BCIALG_1:7;
      k<=n by A4,NAT_1:13;
      then (x,y) to_power m\z= ((x\z,y) to_power k)\y by A3,A5;
      hence (x,y) to_power m\z= (x\z,y) to_power (k+1) by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem
  (x,x\(x\y)) to_power n = (x,y) to_power n
proof
  defpred P[set] means for m holds
  m=$1 & m<= n implies (x,x\(x\y)) to_power m = (x,y) to_power m;
  now (x,x\(x\y)) to_power 0 = x by Th1;
    hence (x,x\(x\y)) to_power 0 = (x,y) to_power 0 by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for
      m holds m=k & m<= n implies (x,x\(x\y)) to_power m = (x,y) to_power m;
      let m;
      assume
A4:   m=k+1 & m<=n;
A5:   (x,x\(x\y)) to_power (k+1) =(x,x\(x\y)) to_power k\(x\(x\y)) by Th4;
      k<=n by A4,NAT_1:13;
      hence (x,x\(x\y)) to_power (k+1)=(x,y) to_power k \(x\(x\y)) by A3,A5
        .=(x\(x\(x\y)),y) to_power k by Th7
        .=(x\y,y) to_power k by BCIALG_1:8
        .=(x,y) to_power k\y by Th7
        .=(x,y) to_power (k+1) by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th9:
  ((0.X,x) to_power n)` = (0.X,x`) to_power n
proof
  defpred P[set] means for m holds m=$1 & m<= n implies
  ((0.X,x) to_power m)` = (0.X,x`) to_power m;
  now ((0.X,x) to_power 0)`= (0.X)` by Th1;
    then ((0.X,x) to_power 0)`= 0.X by BCIALG_1:2;
    hence ((0.X,x) to_power 0)`=(0.X,x`) to_power 0 by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m holds m=k & m<= n
      implies ((0.X,x) to_power m)` = (0.X,x`) to_power m;
      let m;
      assume
A4:   m=k+1 & m<=n;
A5:   ((0.X,x) to_power (k+1))`=((0.X,x) to_power k\x)` by Th4
        .=((0.X,x) to_power k)`\x` by BCIALG_1:9;
      k<=n by A4,NAT_1:13;
      hence ((0.X,x) to_power (k+1))` = ((0.X,x`) to_power k)\x` by A3,A5
        .=(0.X,x`) to_power (k+1) by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th10:
  ((x,y) to_power n,y) to_power m =(x,y) to_power (n+m)
proof
  defpred P[set] means
  for m1 being Element of NAT holds m1=$1 & m1<= n implies
  ((x,y) to_power m1,y) to_power m =(x,y) to_power (m1+m);
A1: P[0] by Th1;
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m1 being Element of NAT st m1=k & m1<=n
      holds((x,y) to_power m1,y) to_power m =(x,y) to_power (m1+m);
      let m1 be Element of NAT;
      assume
A4:   m1=k+1 & m1<=n;
      then k<=n by NAT_1:13;
      then ((x,y) to_power k,y) to_power m =(x,y) to_power (k+m) by A3;
      then (((x,y) to_power k,y) to_power m)\y=(x,y) to_power (k+m+1) by Th4;
      then (((x,y) to_power k)\y,y) to_power m=(x,y) to_power (k+m+1) by Th7;
      hence ((x,y) to_power m1,y) to_power m=(x,y) to_power (m1+m) by A4,Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem
  ((x,y) to_power n,z) to_power m =((x,z) to_power m,y)to_power n
proof
  defpred P[set] means
  for m1 being Element of NAT holds m1=$1 & m1<= n implies
  ((x,y) to_power m1,z) to_power m =((x,z) to_power m,y)to_power m1;
  now
    ((x,y) to_power 0,z)to_power m =(x,z)to_power m by Th1;
    hence ((x,y) to_power 0,z)to_power m
    =((x,z)to_power m,y) to_power 0 by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m1 being Element of NAT st m1=k & m1<=n holds
      ((x,y) to_power m1,z) to_power m =((x,z) to_power m,y)to_power m1;
      let m1 be Element of NAT;
      assume m1=k+1 & m1<=n;
      then k<=n by NAT_1:13;
      then (((x,y) to_power k,z) to_power m)\y
      =((x,z) to_power m,y)to_power k \ y by A3
        .=((x,z) to_power m,y)to_power (k+1) by Th4;
      then ((x,z) to_power m,y)to_power (k+1)
      =((x,y) to_power k\y,z) to_power m by Th7;
      hence ((x,y) to_power (k+1),z) to_power m
      =((x,z) to_power m,y)to_power (k+1) by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th12:
  ((0.X,x) to_power n)``=(0.X,x) to_power n
proof
  defpred P[set] means for m being Element of NAT holds m=$1 & m<=n implies
  (((0.X,x)to_power m)`)`=(0.X,x)to_power m;
  now (((0.X,x)to_power 0)`)`=((0.X)`)` by Th1
      .=(0.X)` by BCIALG_1:def 5
      .=0.X by BCIALG_1:def 5;
    hence (((0.X,x)to_power 0)`)`=(0.X,x)to_power 0 by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for m being Element of NAT st m=k & m<=n holds
      (((0.X,x)to_power m)`)`=(0.X,x)to_power m;
      let m be Element of NAT;
      assume m=k+1 & m<=n;
      then
A4:   k<=n by NAT_1:13;
      (((0.X,x)to_power (k+1))`)` =(((0.X,x)to_power k\x)`)` by Th4
        .=(((0.X,x) to_power k)`\x`)` by BCIALG_1:9
        .=(((0.X,x)to_power k)`)`\((x`)`) by BCIALG_1:9
        .=(0.X,x)to_power k\((x`)`) by A3,A4
        .=(((x`)`)`,x)to_power k by Th7
        .=(x`,x)to_power k by BCIALG_1:8
        .=(0.X,x)to_power k\x by Th7;
      hence (((0.X,x)to_power (k+1))`)` =(0.X,x)to_power (k+1) by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem Th13:
  (0.X,x)to_power (n+m)=((0.X,x)to_power n)\((0.X,x)to_power m)`
proof
  defpred P[set] means for j being Element of NAT holds j=$1 & j<=n implies
  (0.X,x)to_power (j+m)=((0.X,x)to_power j)\((0.X,x)to_power m)`;
  now (0.X,x)to_power (0+m) =(((0.X,x)to_power m)`)` by Th12;
    hence (0.X,x)to_power (0+m)
    =((0.X,x)to_power 0)\((0.X,x)to_power m)` by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for j being Element of NAT st j=k & j<=n holds
      (0.X,x)to_power (j+m)=((0.X,x)to_power j)\((0.X,x)to_power m)`;
      let j be Element of NAT;
      assume j=k+1 & j<=n;
      then
A4:   k<=n by NAT_1:13;
      (0.X,x)to_power (k+m+1)=((0.X,x)to_power (k+m))\x by Th4
        .=(((0.X,x)to_power k)\((0.X,x)to_power m)`)\x by A3,A4
        .=(((0.X,x)to_power k)\x)\((0.X,x)to_power m)` by BCIALG_1:7;
      hence (0.X,x)to_power ((k+1)+m)
      =((0.X,x)to_power (k+1))\((0.X,x)to_power m)` by Th4;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem
  ((0.X,x) to_power (m+n))` = ((0.X,x)to_power m)`\(0.X,x)to_power n
proof
  ((0.X,x)to_power (m+n))`
  =(((0.X,x)to_power m)\((0.X,x)to_power n)`)` by Th13
    .=(((0.X,x)to_power m)`)\(((0.X,x)to_power n)`)` by BCIALG_1:9;
  hence thesis by Th12;
end;

theorem
  ((0.X,(0.X,x)to_power m)to_power n)`=(0.X,x)to_power (m*n)
proof
  defpred P[set] means for j being Element of NAT holds j=$1 & j<=n
  implies ((0.X,(0.X,x)to_power m)to_power j)`=(0.X,x)to_power (m*j);
  now ((0.X,(0.X,x)to_power m)to_power 0)` =(0.X)` by Th1
      .= 0.X by BCIALG_1:def 5;
    hence ((0.X,(0.X,x)to_power m)to_power 0)` =(0.X,x)to_power (m*0) by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A3:   for j being Element of NAT st j=k & j<=n holds
      ((0.X,(0.X,x)to_power m)to_power j)`=(0.X,x)to_power (m*j);
      let j be Element of NAT;
      assume j=k+1 & j<=n;
      then
A4:   k<=n by NAT_1:13;
      ((0.X,(0.X,x)to_power m)to_power (k+1))`
      =(((0.X,(0.X,x)to_power m)to_power k)\((0.X,x)to_power m))`by Th4
        .=((0.X,(0.X,x)to_power m)to_power k)`\((0.X,x)to_power m)`
      by BCIALG_1:9
        .=((0.X,x)to_power (m*k))\((0.X,x)to_power m)`by A3,A4
        .=(0.X,x)to_power (m*k+m)by Th13;
      hence ((0.X,(0.X,x)to_power m)to_power (k+1))`
      =(0.X,x)to_power (m*(k+1));
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem
  (0.X,x)to_power m=0.X implies(0.X,x)to_power (m*n)=0.X
proof
  assume
A1: (0.X,x)to_power m=0.X;
  defpred P[set] means for j being Element of NAT holds j=$1 & j<=n
  implies (0.X,x)to_power (m*j)=0.X;
A2: P[0] by Th1;
A3: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A4:   for j st j=k & j<=n holds (0.X,x)to_power (m*j)=0.X;
      let j;
      assume j=k+1 & j<=n;
      then
A5:   k<=n by NAT_1:13;
      (0.X,x)to_power (m*(k+1)) = (0.X,x)to_power (m*k+m)
        .= ((0.X,x)to_power (m*k),x)to_power m by Th10
        .= (0.X,x)to_power m by A4,A5;
      hence (0.X,x)to_power (m*(k+1))=0.X by A1;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A2,A3);
  hence thesis;
end;

theorem
  x\y=x implies (x,y) to_power n = x
proof
  assume
A1: x\y=x;
  defpred P[set] means for m holds m=$1 & m<=n implies (x,y) to_power m = x;
A2: P[0] by Th1;
A3: for k st P[k] holds P[k+1]
  proof
    now
      let k;
      assume
A4:   for m holds m=k & m<= n implies (x,y) to_power m = x;
      let m;
      assume
A5:   m=k+1 & m<=n;
A6:   (x,y) to_power (k+1)=(x,y) to_power k \ y by Th4;
      k<=n by A5,NAT_1:13;
      hence (x,y) to_power (k+1)=x by A1,A4,A6;
    end;
    hence thesis;
  end;
  for n holds P[n] from NAT_1:sch 1(A2,A3);
  hence thesis;
end;

theorem
  (0.X,x\y) to_power n=((0.X,x) to_power n)\((0.X,y) to_power n)
proof
  defpred P[set] means for m holds m=$1 & m<=n implies
  (0.X,x\y) to_power m=((0.X,x) to_power m)\((0.X,y) to_power m);
  now (0.X)`=0.X by BCIALG_1:def 5;
    then (0.X,x\y) to_power 0=(0.X)` by Th1;
    then (0.X,x\y) to_power 0=((0.X,x) to_power 0)\0.X by Th1;
    hence (0.X,x\y) to_power 0
    =((0.X,x) to_power 0)\((0.X,y) to_power 0)by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A3: for m holds m=k & m<= n implies
    (0.X,x\y) to_power m=((0.X,x) to_power m)\((0.X,y) to_power m);
    let m;
    assume
A4: m=k+1 & m<=n;
    then k<=n by NAT_1:13;
    then (0.X,x\y) to_power k
    =((0.X,x) to_power k)\((0.X,y) to_power k) by A3;
    then (0.X,x\y) to_power (k+1)
    =(((0.X,x) to_power k)\((0.X,y) to_power k))\(x\y)by Th4
      .= ((0.X,x) to_power k)\(x\y)\((0.X,y) to_power k)by BCIALG_1:7
      .= (((x\y)`,x) to_power k)\((0.X,y) to_power k)by Th7
      .=((x`\y`,x) to_power k)\((0.X,y) to_power k)by BCIALG_1:9
      .=((x`,x) to_power k)\y`\((0.X,y) to_power k)by Th7
      .=((x`,x) to_power k)\((0.X,y) to_power k)\y` by BCIALG_1:7
      .=((0.X,x) to_power k)\x\((0.X,y) to_power k)\y` by Th7;
    then (0.X,x\y) to_power (k+1)
    =((0.X,x) to_power (k+1))\((0.X,y) to_power k)\y` by Th4
      .=((0.X,x) to_power (k+1))\y`\((0.X,y) to_power k)by BCIALG_1:7
      .=(((y`)`,x) to_power (k+1))\((0.X,y) to_power k)by Th7
      .=(((y`)`\((0.X,y) to_power k),x) to_power (k+1))by Th7
      .=(((0.X,y) to_power k)`\y`,x) to_power (k+1)by BCIALG_1:7
      .=((((0.X,y) to_power k)\y)`,x) to_power (k+1)by BCIALG_1:9
      .=(((0.X,y) to_power (k+1))`,x) to_power (k+1)by Th4;
    hence thesis by A4,Th7;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

::P20-P22

theorem
  x<=y implies (x,z) to_power n <= (y,z) to_power n
proof
  assume
A1: x<=y;
  defpred P[set] means for m being Element of NAT holds m=$1 & m<=n
  implies (x,z) to_power m <= (y,z) to_power m;
  now (x,z) to_power 0 <= y by A1,Th1;
    hence (x,z) to_power 0 <= (y,z) to_power 0 by Th1;
  end;
  then
A2: P[0];
A3: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A4: for m being Element of NAT holds m=k & m<= n implies
    (x,z) to_power m <= (y,z) to_power m;
    let m be Element of NAT;
    assume
A5: m=k+1 & m<=n;
    then k<=n by NAT_1:13;
    then (x,z) to_power k <= (y,z) to_power k by A4;
    then (x,z) to_power k\z<=(y,z) to_power k \ z by BCIALG_1:5;
    then (x,z) to_power (k+1)<=(y,z) to_power k\z by Th4;
    hence thesis by A5,Th4;
  end;
  for n holds P[n] from NAT_1:sch 1(A2,A3);
  hence thesis;
end;

theorem
  x<=y implies (z,y) to_power n <= (z,x) to_power n
proof
  assume
A1: x<=y;
  defpred P[set] means for m being Element of NAT holds m=$1 & m<=n
  implies (z,y) to_power m <= (z,x) to_power m;
  now z\z=0.X by BCIALG_1:def 5;
    then z<=z by BCIALG_1:def 11;
    then (z,y) to_power 0 <= z by Th1;
    hence (z,y) to_power 0 <= (z,x) to_power 0 by Th1;
  end;
  then
A2: P[0];
A3: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A4: for m holds m=k & m<= n implies (z,y) to_power m <= (z,x) to_power m;
    let m;
    assume
A5: m=k+1 & m<=n;
    then k<=n by NAT_1:13;
    then (z,y) to_power k <= (z,x) to_power k by A4;
    then (z,y) to_power k\y <= (z,x) to_power k\y by BCIALG_1:5;
    then (z,y) to_power (k+1)<= (z,x) to_power k\y by Th4;
    then
A6: ((z,y) to_power (k+1))\((z,x) to_power k\y)=0.X by BCIALG_1:def 11;
    ((z,x) to_power k)\y<=(z,x) to_power k\x by A1,BCIALG_1:5;
    then (z,x) to_power k\y<=(z,x) to_power (k+1) by Th4;
    then ((z,x) to_power k\y)\((z,x) to_power (k+1))=0.X by BCIALG_1:def 11;
    then ((z,y) to_power (k+1))\((z,x) to_power (k+1))=0.X by A6,BCIALG_1:3;
    hence thesis by A5,BCIALG_1:def 11;
  end;
  for n holds P[n] from NAT_1:sch 1(A2,A3);
  hence thesis;
end;

theorem
  ((x,z) to_power n)\((y,z) to_power n) <= x\y
proof
  defpred P[set] means for m being Element of NAT holds m=$1 & m<=n
  implies ((x,z) to_power m)\((y,z) to_power m) <= x\y;
  now (x\y)\(x\y)=0.X by BCIALG_1:def 5;
    then x\y <= x\y by BCIALG_1:def 11;
    then ((x,z) to_power 0)\y <= x\y by Th1;
    hence ((x,z) to_power 0)\((y,z) to_power 0) <= x\y by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A3: for m being Element of NAT holds m=k & m<= n
    implies((x,z) to_power m)\((y,z) to_power m) <= x\y;
    let m be Element of NAT;
    assume
A4: m=k+1 & m<=n;
    then k<=n by NAT_1:13;
    then ((x,z) to_power k)\((y,z) to_power k) <= x\y by A3;
    then (((x,z) to_power k)\((y,z) to_power k))\(x\y)=0.X by BCIALG_1:def 11;
    then (((x,z) to_power k)\(x\y))\((y,z) to_power k)=0.X by BCIALG_1:7;
    then (((x,z) to_power k)\(x\y))\z\(((y,z) to_power k)\z)=0.X by BCIALG_1:4;
    then (((x,z) to_power k)\z)\(x\y)\(((y,z) to_power k)\z)=0.X by BCIALG_1:7;
    then ((x,z) to_power (k+1))\(x\y)\(((y,z) to_power k)\z)=0.X by Th4;
    then ((x,z) to_power (k+1))\(x\y)\((y,z) to_power (k+1))=0.X by Th4;
    then ((x,z) to_power (k+1))\((y,z) to_power (k+1))\(x\y)=0.X by BCIALG_1:7;
    hence thesis by A4,BCIALG_1:def 11;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

theorem
  (((x,x\y) to_power n),y\x) to_power n <= x
proof
  defpred P[set] means for m being Element of NAT holds m=$1 & m<=n
  implies (((x,x\y) to_power m),y\x) to_power m <= x;
  now x\x=0.X by BCIALG_1:def 5;
    then x<=x by BCIALG_1:def 11;
    then (x,y\x) to_power 0<=x by Th1;
    hence (((x,x\y) to_power 0),y\x) to_power 0<=x by Th1;
  end;
  then
A1: P[0];
A2: for k st P[k] holds P[k+1]
  proof
    let k;
    assume
A3: for m being Element of NAT holds m=k & m<= n
    implies (((x,x\y) to_power m),y\x) to_power m <= x;
    let m be Element of NAT;
    assume
A4: m=k+1 & m<=n;
    then k<=n by NAT_1:13;
    then (((x,x\y) to_power k),y\x) to_power k <= x by A3;
    then ((((x,x\y) to_power k),y\x) to_power k)\x=0.X by BCIALG_1:def 11;
    then ((((x,x\y) to_power k)\x,y\x) to_power k)\(y\x)=(y\x)`by Th7;
    then ((((x,x\y) to_power k)\x,y\x)to_power (k+1))\(x\y)
    =(y\x)`\(x\y)by Th4;
    then (((x,x\y) to_power k)\x\(x\y),y\x) to_power (k+1)=(y\x)`\(x\y)by Th7;
    then (((x,x\y) to_power k)\(x\y)\x,y\x) to_power (k+1)=(y\x)`\(x\y)
    by BCIALG_1:7;
    then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1)=(y\x)`\(x\y)by Th4;
    then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1)
    =(y\y)\(y\x)\(x\y)by BCIALG_1:def 5;
    then (((x,x\y) to_power (k+1))\x,y\x) to_power (k+1)=0.X by BCIALG_1:1;
    then (((x,x\y) to_power (k+1),y\x) to_power (k+1))\x=0.X by Th7;
    hence thesis by A4,BCIALG_1:def 11;
  end;
  for n holds P[n] from NAT_1:sch 1(A1,A2);
  hence thesis;
end;

notation
  let X,a;
  synonym a is minimal for a is atom;
end;

::P17   proposition 1.1.10

definition
  let X,a;
  attr a is positive means
  :Def2:
  0.X <= a;
  attr a is least means

  for x holds a<=x;
  attr a is maximal means
  :Def4:
  for x holds a<=x implies x=a;
  attr a is greatest means
  :Def5:
  for x holds x<=a;
end;

Lm1: a is minimal iff for x holds x<=a implies x=a
proof
  thus a is minimal implies for x holds x<=a implies x=a
  proof
    assume
A1: a is minimal;
    let x;
    assume x<=a;
    then x\a=0.X by BCIALG_1:def 11;
    hence thesis by A1,BCIALG_1:def 14;
  end;
  assume
A2: for x holds x<=a implies x=a;
  now
    let y;
    assume y\a=0.X;
    then y<=a by BCIALG_1:def 11;
    hence y=a by A2;
  end;
  hence thesis by BCIALG_1:def 14;
end;

Lm2: 0.X is positive
proof
  (0.X)`=0.X by BCIALG_1:2;
  then 0.X <= 0.X by BCIALG_1:def 11;
  hence thesis by Def2;
end;

registration
  let X;
  cluster positive Element of X;
  existence
  proof
    take x=0.X;
    thus thesis by Lm2;
  end;
end;

Lm3: 0.X is minimal
proof
  for x st x\0.X=0.X holds x=0.X by BCIALG_1:2;
  hence thesis by BCIALG_1:def 14;
end;

registration
  let X;
  cluster 0.X -> positive minimal;
  coherence by Lm2,Lm3;
end;

theorem
  a is minimal iff for x holds a\x=x`\a`
proof
  thus a is minimal implies for x holds a\x=x`\a`
  proof
    assume
A1: a is minimal;
    let x;
    x\(x\a)\a=0.X by BCIALG_1:1;
    then x\(x\a)<=a by BCIALG_1:def 11;
    then
A2: (a\x)\(x`\a`)=((x\(x\a))\x)\(x`\a`)by A1,Lm1
      .=((x\x)\(x\a))\(x`\a`) by BCIALG_1:7
      .=((x\a)`)\(x`\a`) by BCIALG_1:def 5
      .=((x\a)`)\((x\a)`) by BCIALG_1:9
      .=0.X by BCIALG_1:def 5;
    (x`\a`)\(a\x)=0.X by BCIALG_1:1;
    hence thesis by A2,BCIALG_1:def 7;
  end;
  thus (for x holds a\x=x`\a`) implies a is minimal
  proof
    assume
A3: for x holds a\x=x`\a`;
    now
      let x;
      assume x<=a;
      then
A4:   x\a=0.X by BCIALG_1:def 11;
      a\x=x`\a` by A3;
      then a\x=(0.X)` by A4,BCIALG_1:9;
      then a\x=0.X by BCIALG_1:def 5;
      hence a=x by A4,BCIALG_1:def 7;
    end;
    hence thesis by Lm1;
  end;
end;

theorem
  x` is minimal iff (for y holds y<=x implies x` = y`)
proof
  thus x` is minimal implies (for y holds y<=x implies x` = y`)
  proof
    assume
A1: x` is minimal;
    let y;
    assume y<=x;
    then y\x=0.X by BCIALG_1:def 11;
    then (y\x)`=0.X by BCIALG_1:def 5;
    then y`\x`=0.X by BCIALG_1:9;
    then y`<=x` by BCIALG_1:def 11;
    hence thesis by A1,Lm1;
  end;
  thus (for y holds y<=x implies x` = y`)implies x` is minimal
  proof
    assume
A2: for y holds y<=x implies x` = y`;
    now
      let xx be Element of X;
      assume xx<=x`;
      then
A3:   xx\x`=0.X by BCIALG_1:def 11;
      then (xx\x`)`=0.X by BCIALG_1:def 5;
      then xx`\((x`)`)=0.X by BCIALG_1:9;
      then (xx`\((x`)`))`=0.X by BCIALG_1:def 5;
      then ((xx`)`)\(((x`)`)`)=0.X by BCIALG_1:9;
      then ((xx`)`)\x`=0.X by BCIALG_1:8;
      then (xx`\x)`=0.X by BCIALG_1:9;
      then (x`\xx)`=0.X by BCIALG_1:7;
      then (xx\xx)\(x`\xx)=0.X by BCIALG_1:def 5;
      then (xx\x`)`=0.X by BCIALG_1:def 3;
      then xx`\((x`)`)=0.X by BCIALG_1:9;
      then xx`\x\(((x`)`)\x)=0.X by BCIALG_1:4;
      then xx`\x\0.X=0.X by BCIALG_1:1;
      then xx`\x=0.X by BCIALG_1:2;
      then xx`<=x by BCIALG_1:def 11;
      then (xx`)`=x` by A2;
      then 0.X = x`\xx by BCIALG_1:1;
      hence xx=x` by A3,BCIALG_1:def 7;
    end;
    hence thesis by Lm1;
  end;
end;

theorem
  x` is minimal iff for y,z holds((((x\z)\(y\z))`)` = y`\x`)
proof
  thus x` is minimal implies for y,z holds((((x\z)\(y\z))`)` = y`\x`)
  proof
    assume
A1: x` is minimal;
    let y,z;
A2: (((x\z)\(y\z))`)` = ((x\z)`\(y\z)`)` by BCIALG_1:9
      .= ((x`\z`)\((y\z)`))` by BCIALG_1:9;
    y`\(x\y)\x`=0.X by BCIALG_1:def 3;
    then y`\(x\y)<=x` by BCIALG_1:def 11;
    then (((x\z)\(y\z))`)` = ((y`\(x\y)\z`)\(y\z)`)` by A1,A2,Lm1
      .= ((y`\z`\(x\y))\(y\z)`)` by BCIALG_1:7
      .= (((y\z)`\(x\y))\(y\z)`)` by BCIALG_1:9
      .= (((y\z)`)\((y\z)`)\(x\y))` by BCIALG_1:7
      .= ((x\y)`)` by BCIALG_1:def 5
      .= (x`\y`)` by BCIALG_1:9
      .= ((y`)`\x)` by BCIALG_1:7
      .= ((y`)`)`\x` by BCIALG_1:9
      .= y`\x` by BCIALG_1:8;
    hence thesis;
  end;
  thus (for y,z holds (((x\z)\(y\z))`)` = y`\x`) implies x` is minimal
  proof
    assume
A3: for y,z holds (((x\z)\(y\z))`)` = y`\x`;
    now
      let x1 be Element of X;
      assume x1<=x`;
      then
A4:   x1\x`=0.X by BCIALG_1:def 11;
      then (x1`\x`)\(x1`\x1)=0.X by BCIALG_1:4;
      then ((((x\0.X)\(x1\0.X))`)`)\(x1`\x1)=0.X by A3;
      then ((x1`\x1)`)\(((x\0.X)\(x1\0.X))`)=0.X by BCIALG_1:7;
      then ((x1`\x1)`)\((x\(x1\0.X))`)=0.X by BCIALG_1:2;
      then ((x1`\x1)`)\((x\x1)`)=0.X by BCIALG_1:2;
      then (((x1`)`)\x1`)\((x\x1)`)=0.X by BCIALG_1:9;
      then (((x1`)`)\x1`)\(x`\x1`)=0.X by BCIALG_1:9;
      then (((x1`)`)\x`)`=0.X by BCIALG_1:def 3;
      then (((x1`)`)`)\((x`)`)=0.X by BCIALG_1:9;
      then x1`\((x`)`)=0.X by BCIALG_1:8;
      then (((x`)`)`)\x1=0.X by BCIALG_1:7;
      then x`\x1=0.X by BCIALG_1:8;
      hence x1=x` by A4,BCIALG_1:def 7;
    end;
    hence thesis by Lm1;
  end;
end;

theorem
  0.X is maximal implies for a holds a is minimal
proof
  assume
A1: 0.X is maximal;
  let a;
  now
    let x;
    assume x<=a;
    then
A2: x\a=0.X by BCIALG_1:def 11;
    then (a\x)`=0.X by BCIALG_1:6;
    then 0.X <= a\x by BCIALG_1:def 11;
    then 0.X = a\x by A1,Def4;
    hence x=a by A2,BCIALG_1:def 7;
  end;
  hence thesis by Lm1;
end;

theorem
  (ex x st x is greatest) implies for a holds a is positive
proof
  given x such that
A1: x is greatest;
  0.X<=x by A1,Def5;
  then
A2: x`=0.X by BCIALG_1:def 11;
  let a;
  a<=x by A1,Def5;
  then a\x=0.X by BCIALG_1:def 11;
  then (a\x)`=0.X by BCIALG_1:def 5;
  then a`\0.X=0.X by A2,BCIALG_1:9;
  then a`=0.X by BCIALG_1:2;
  then 0.X<=a by BCIALG_1:def 11;
  hence thesis by Def2;
end;

theorem Th28:
  x\(x``) is positive Element of X
proof
  (x\((x`)`))` = x`\(((x`)`)`) by BCIALG_1:9
    .=x`\x` by BCIALG_1:8
    .=0.X by BCIALG_1:def 5;
  then 0.X<=x\((x`)`) by BCIALG_1:def 11;
  hence thesis by Def2;
end;

theorem
  a is minimal iff a`` = a
proof
  thus a is minimal implies a`` = a
  proof
    assume
A1: a is minimal;
    (a`)`\a=0.X by BCIALG_1:1;
    then (a`)` <= a by BCIALG_1:def 11;
    hence thesis by A1,Lm1;
  end;
  assume
A2: a`` = a;
  now
    let x;
    assume x<=a;
    then
A3: x\a=0.X by BCIALG_1:def 11;
    a\x=x`\a` by A2,BCIALG_1:7;
    then a\x=(0.X)` by A3,BCIALG_1:9;
    then a\x=0.X by BCIALG_1:def 5;
    hence x=a by A3,BCIALG_1:def 7;
  end;
  hence thesis by Lm1;
end;

theorem Th30:
  a is minimal iff ex x st a=x`
proof
  thus a is minimal implies ex x st a=x`
  proof
    assume
A1: a is minimal;
    take x=a`;
    x`\a=0.X by BCIALG_1:1;
    then x` <= a by BCIALG_1:def 11;
    hence thesis by A1,Lm1;
  end;
  given x such that
A2: a=x`;
  now
    let y;
    assume y<=a;
    then
A3: y\a=0.X by BCIALG_1:def 11;
    then a\y=y\x`\y\x by A2,BCIALG_1:7;
    then a\y=y\y\x`\x by BCIALG_1:7;
    then a\y=(x`)`\x by BCIALG_1:def 5;
    then a\y=0.X by BCIALG_1:1;
    hence a=y by A3,BCIALG_1:def 7;
  end;
  hence thesis by Lm1;
end;

:: p38

definition
  let X,x;
  attr x is nilpotent means
  :Def6:
  ex k being non empty Element of NAT st (0.X,x) to_power k = 0.X;
end;

definition
  let X;
  attr X is nilpotent means

  for x being Element of X holds x is nilpotent;
end;

definition
  let X,x;
  assume
A1: x is nilpotent;
  func ord x -> non empty Element of NAT means
  :Def8:
  (0.X,x) to_power it = 0.X &
  for m being Element of NAT st (0.X,x) to_power m=0.X & m <> 0 holds it <= m;
  existence
  proof
    defpred P[Nat] means ex w be Element of NAT st w=$1 &
    (0.X,x)to_power w = 0.X & w<>0;
    consider k being non empty Element of NAT such that
A2: (0.X,x) to_power k = 0.X by A1,Def6;
A3: ex n being Nat st P[n] by A2;
    consider k being Nat such that
A4: P[k] and
A5: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A3);
    reconsider k as non empty Element of NAT by A4;
    take k;
    thus thesis by A4,A5;
  end;
  uniqueness
  proof
    let n1,n2 be non empty Element of NAT;
    assume that
A6: (0.X,x) to_power n1 = 0.X &
    for m being Element of NAT st (0.X,x)to_power m=0.X&m <> 0 holds n1<=m and
A7: (0.X,x) to_power n2 = 0.X &
    for m being Element of NAT st (0.X,x)to_power m=0.X&m <> 0 holds n2<=m;
    n1 <= n2 & n2 <= n1 by A6,A7;
    hence n1 = n2 by XXREAL_0:1;
  end;
  correctness;
end;

registration
  let X;
  cluster 0.X -> nilpotent;
  coherence
  proof
    (0.X,0.X) to_power 1 = 0.X by Th6;
    hence thesis by Def6;
  end;
end;

theorem :: P39
  x is positive Element of X iff x is nilpotent & ord x=1
proof
  thus x is positive Element of X implies x is nilpotent&ord x=1
  proof
    assume x is positive Element of X;
    then 0.X<=x by Def2;
    then
A1: x`=0.X by BCIALG_1:def 11; thus
A2: x is nilpotent
    proof
      set k=1;
      take k;
      thus thesis by A1,Th2;
    end;
    thus ord x=1
    proof
      set k=1;
      reconsider k as non empty Element of NAT;
A3:   (0.X,x) to_power k=0.X by A1,Th2;
      for m being Element of NAT st (0.X,x)to_power m=0.X&m <> 0
      holds k<= m by NAT_1:14;
      hence thesis by A2,A3,Def8;
    end;
  end;
  assume x is nilpotent & ord x=1;
  then (0.X,x) to_power 1 = 0.X by Def8;
  then x`=0.X by Th2;
  then 0.X<=x by BCIALG_1:def 11;
  hence thesis by Def2;
end;

theorem
  X is BCK-algebra iff for x holds ord x=1 & x is nilpotent
proof
  thus X is BCK-algebra implies for x being Element of X
  holds ord x=1&x is nilpotent
  proof
    assume
A1: X is BCK-algebra;
    let x be Element of X;
A2: x`=0.X by A1,BCIALG_1:def 8;
    then (0.X,x)to_power 1=0.X by Th2;
    then
A3: x is nilpotent by Def6;
    set k=1;
    reconsider k as non empty Element of NAT;
A4: (0.X,x) to_power k=0.X by A2,Th2;
    for m being Element of NAT st (0.X,x)to_power m=0.X&m <> 0
    holds k<= m by NAT_1:14;
    hence thesis by A3,A4,Def8;
  end;
  assume
A5: for x holds ord x = 1&x is nilpotent;
  now
    let x;
    ord x =1&x is nilpotent by A5;
    then (0.X,x) to_power 1 = 0.X by Def8;
    hence x` =0.X by Th2;
  end;
  hence thesis by BCIALG_1:def 8;
end;

theorem
  (0.X,x`) to_power n is minimal
proof
  (0.X,x`) to_power n=((0.X,x) to_power n)` by Th9;
  hence thesis by Th30;
end;

theorem
  x is nilpotent implies ord x = ord (x`)
proof
  assume
A1: x is nilpotent;
  then consider k being non empty Element of NAT such that
A2: (0.X,x) to_power k = 0.X by Def6;
A3: x` is nilpotent
  proof
    take k;
    (0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
      .=0.X by A2,BCIALG_1:def 5;
    hence thesis;
  end;
  set k=ord x;
  ord (x`)=k
  proof
A4: (0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
      .=(0.X)` by A1,Def8
      .=0.X by BCIALG_1:def 5;
    now
      let m be Element of NAT;
      assume
A5:   (0.X,x`)to_power m=0.X&m <> 0;
      then ((0.X,x)to_power m)`=0.X by Th9;
      then (((0.X,x)to_power m)`)`=0.X by BCIALG_1:def 5;
      then (0.X,x)to_power m=0.X by Th12;
      hence k<=m by A1,A5,Def8;
    end;
    hence thesis by A3,A4,Def8;
  end;
  hence thesis;
end;

begin :: Congruence and Quotient Algebras P58-65

definition
  let X be BCI-algebra;
  mode Congruence of X -> Equivalence_Relation of X means
    :Def9:
    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
  proof
    reconsider P = id the carrier of X as Equivalence_Relation of X;
    take P;
    let x,y,u,v be Element of X;
    assume [x,y] in P&[u,v]in P;
    then x in the carrier of X & x=y & u in the carrier of X&u=v
    by RELAT_1:def 10;
    hence thesis by RELAT_1:def 10;
  end;
end;

:: Left Congruence

definition
  let X be BCI-algebra;
  mode L-congruence of X -> Equivalence_Relation of X means
    :Def10:
    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
  proof
    reconsider P = id the carrier of X as Equivalence_Relation of X;
    take P;
    let x,y be Element of X;
    assume
A1: [x,y] in P;
    let u be Element of X;
    u\x=u\y & u\x in the carrier of X by A1,RELAT_1:def 10;
    hence thesis by RELAT_1:def 10;
  end;
end;

:: Right Congruence

definition
  let X be BCI-algebra;
  mode R-congruence of X -> Equivalence_Relation of X means
    :Def11:
    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
  proof
    reconsider P = id the carrier of X as Equivalence_Relation of X;
    take P;
    let x,y be Element of X;
    assume
A1: [x,y] in P;
    let u be Element of X;
    x\u=y\u & x\u in the carrier of X by A1,RELAT_1:def 10;
    hence thesis by RELAT_1:def 10;
  end;
end;

::Ideal Congruence

definition
  let X be BCI-algebra,A be Ideal of X;
  mode I-congruence of X,A -> Relation of X means
    :Def12:
    for x,y being Element of X holds [x,y] in it iff x\y in A & y\x in A;
  existence
  proof
    defpred PP[set,set] means ex x,y being Element of X st x=$1&y=$2
    &x\y in A & y\x in A;
    consider P being Relation of X such that
A1: for x2,y2 being set holds [x2,y2] in P iff x2 in the carrier of X&
    y2 in the carrier of X&PP[x2,y2] from RELSET_1:sch 1;
    take P;
    let x2,y2 be Element of X;
    thus [x2,y2] in P implies x2\y2 in A & y2\x2 in A
    proof
      [x2,y2] in P implies ex x1,y1 being Element of X
      st x1=x2&y1=y2&x1\y1 in A & y1\x1 in A by A1;
      hence thesis;
    end;
    thus x2\y2 in A & y2\x2 in A implies [x2,y2] in P by A1;
  end;
end;

registration
  let X be BCI-algebra, A be Ideal of X;
  cluster -> total symmetric transitive I-congruence of X,A;
  coherence
  proof
    for RI being I-congruence of X,A holds RI is Equivalence_Relation of X
    proof
      let RI be I-congruence of X,A;
      reconsider RI as Relation of X;
   RI is_reflexive_in the carrier of X
      proof
        for x being set st x in the carrier of X holds [x,x] in RI
        proof
          let x be set;
          assume x in the carrier of X;
          then reconsider x as Element of X;
          0.X in A by BCIALG_1:def 18;
          then x\x in A by BCIALG_1:def 5;
          hence thesis by Def12;
        end;
        hence thesis by RELAT_2:def 1;
      end;
      then
A2:   field RI = the carrier of X by ORDERS_1:98;
A4:   RI is symmetric
      proof
        for x,y being set st x in the carrier of X &
        y in the carrier of X & [x,y] in RI holds [y,x] in RI
        proof
          let x,y be set;
          assume
A5:       x in the carrier of X & y in the carrier of X & [x,y] in RI;
          then reconsider x,y as Element of X;
          x\y in A & y\x in A by A5,Def12;
          hence thesis by Def12;
        end;
        then RI is_symmetric_in the carrier of X by RELAT_2:def 3;
        hence thesis by A2,RELAT_2:def 11;
      end;
      RI is transitive
      proof
        for x,y,z being set st [x,y] in RI&[y,z] in RI holds [x,z] in RI
        proof
          let x,y,z be set;
          assume
A6:       [x,y] in RI& [y,z] in RI;
          then reconsider x,y,z as Element of X by ZFMISC_1:106;
A7:       x\y in A&y\x in A & y\z in A&z\y in A by A6,Def12;
          (x\z\(x\y))\(y\z)=0.X by BCIALG_1:1;
          then (x\z\(x\y))\(y\z) in A by BCIALG_1:def 18;
          then x\z\(x\y) in A by A7,BCIALG_1:def 18;
          then
A8:       x\z in A by A7,BCIALG_1:def 18;
          (z\x\(y\x))\(z\y)=0.X by BCIALG_1:def 3;
          then (z\x\(y\x))\(z\y) in A by BCIALG_1:def 18;
          then z\x\(y\x) in A by A7,BCIALG_1:def 18;
          then z\x in A by A7,BCIALG_1:def 18;
          hence thesis by A8,Def12;
        end;
        hence thesis by RELAT_2:48;
      end;
      hence thesis by A2,A4,EQREL_1:16;
    end;
    hence thesis;
  end;
end;

definition
  let X be BCI-algebra;
  func IConSet(X) means
  :Def13:
  for A1 being set holds
  A1 in it iff ex I being Ideal of X st A1 is I-congruence of X,I;
  existence
  proof
    defpred P[set] means ex I being Ideal of X st $1 is I-congruence of X,I;
    consider Y being set such that
A1: for x being set holds
    x in Y iff x in bool [:the carrier of X,the carrier of X:] & P[x]
    from XBOOLE_0:sch 1;
    take Y;
    let x be set;
    thus x in Y implies
    ex I being Ideal of X st x is I-congruence of X,I by A1;
    given I being Ideal of X such that
A2: x is I-congruence of X,I;
    thus thesis by A1,A2;
  end;
  uniqueness
  proof
    let A1, A2 be set such that
A3: for x being set holds x in A1 iff
    ex I being Ideal of X st x is I-congruence of X,I and
A4: for x being set holds x in A2 iff
    ex I being Ideal of X st x is I-congruence of X,I;
    defpred P[set] means ex I being Ideal of X st $1 is I-congruence of X,I;
A5: for x being set holds x in A1 iff P[x] by A3;
A6: for x being set holds x in A2 iff P[x] by A4;
    A1 = A2 from XBOOLE_0:sch 2(A5,A6);
    hence thesis;
  end;
end;

definition
  let X be BCI-algebra;
  func ConSet(X) equals

  {R where R is Congruence of X:not contradiction};
  coherence;
  func LConSet(X) equals

  {R where R is L-congruence of X:not contradiction};
  coherence;
  func RConSet(X) equals

  {R where R is R-congruence of X:not contradiction};
  coherence;
end;

reserve R1,R2,R for Equivalence_Relation of X;
reserve RI for I-congruence of X,I;
reserve E for Congruence of X;
reserve RC for R-congruence of X;
reserve LC for L-congruence of X;

:: huang-P58:P1.5.1

theorem
  for X,E holds Class(E,0.X) is closed Ideal of X
proof
  let X,E;
A1: [0.X,0.X] in E by EQREL_1:11;
  Class(E,0.X) is Ideal of X
  proof
A2: 0.X in Class(E,0.X) by A1,EQREL_1:26;
    now
      let x,y be Element of X;
      assume x\y in Class(E,0.X) & y in Class(E,0.X);
      then
A3:   [0.X,x\y] in E & [0.X,y] in E by EQREL_1:26;
      [x,x] in E by EQREL_1:11;
      then [x\0.X,x\y] in E by A3,Def9;
      then [x,x\y] in E by BCIALG_1:2;
      then [x\y,x] in E by EQREL_1:12;
      then [0.X,x] in E by A3,EQREL_1:13;
      hence x in Class(E,0.X)by EQREL_1:26;
    end;
    hence thesis by A2,BCIALG_1:def 18;
  end;
  then reconsider Rx=Class(E,0.X) as Ideal of X;
  Rx is closed
  proof
    now
      let x be Element of Rx;
      [0.X,x] in E by EQREL_1:26;
      then [(0.X)`,x`] in E by A1,Def9;
      then [0.X,x`] in E by BCIALG_1:def 5;
      hence x` in Class(E,0.X) by EQREL_1:26;
    end;
    hence thesis by BCIALG_1:def 19;
  end;
  hence thesis;
end;

theorem Th36:
  R is Congruence of X iff R is R-congruence of X&R is L-congruence of X
proof
  R is reflexive symmetric transitive & field R = the carrier of X
  by EQREL_1:16;
  then
A1: R is_reflexive_in the carrier of X & R is_symmetric_in the carrier of X &
  R is_transitive_in the carrier of X by RELAT_2:def 9,def 11,def 16;
  thus R is Congruence of X implies R is R-congruence of X&R is L-congruence
  of X
  proof
    assume
A2: R is Congruence of X;
    thus R is R-congruence of X
    proof
      let x,y be Element of X;
      assume
A3:   [x,y] in R;
      let u be Element of X;
      [u,u] in R by A1,RELAT_2:def 1;
      hence thesis by A2,A3,Def9;
    end;
    let x,y be Element of X;
    assume
A4: [x,y] in R;
    let u be Element of X;
    [u,u] in R by A1,RELAT_2:def 1;
    hence thesis by A2,A4,Def9;
  end;
  assume
A5: R is R-congruence of X&R is L-congruence of X;
  now
    let x,y,u,v be Element of X;
    assume [x,y] in R & [u,v]in R;
    then [x\u,y\u] in R & [y\u,y\v] in R by A5,Def10,Def11;
    hence [x\u,y\v] in R by A1,RELAT_2:def 8;
  end;
  hence thesis by Def9;
end;

theorem Th37:
  RI is Congruence of X
proof
  RI is reflexive symmetric transitive
  & field RI = the carrier of X by EQREL_1:16;
  then
A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;
  now
    let x,y,u,v be Element of X;
    assume [x,y] in RI&[u,v]in RI;
    then
A2: x\y in I&y\x in I&u\v in I&v\u in I by Def12;
    (x\u\(y\u))\(x\y)=0.X & (y\u\(x\u))\(y\x)=0.X by BCIALG_1:def 3;
    then (x\u\(y\u))\(x\y) in I &(y\u\(x\u))\(y\x) in I by BCIALG_1:def 18;
    then x\u\(y\u) in I &y\u\(x\u) in I by A2,BCIALG_1:def 18;
    then
A3: [x\u,y\u] in RI by Def12;
    (y\u\(y\v))\(v\u)=0.X & (y\v\(y\u))\(u\v)=0.X by BCIALG_1:1;
    then (y\u\(y\v))\(v\u) in I &(y\v\(y\u))\(u\v) in I by BCIALG_1:def 18;
    then y\u\(y\v) in I & y\v\(y\u) in I by A2,BCIALG_1:def 18;
    then [y\u,y\v] in RI by Def12;
    hence [x\u,y\v] in RI by A1,A3,RELAT_2:def 8;
  end;
  hence thesis by Def9;
end;

definition
  let X be BCI-algebra, I be Ideal of X;
  redefine mode I-congruence of X,I -> Congruence of X;
  coherence by Th37;
end;

theorem Th38:
  Class(RI,0.X) c= I
proof
  let x be set;
  assume
A1: x in Class(RI,0.X);
  then consider y being set such that
A2: [y,x] in RI & y in {0.X} by RELAT_1:def 13;
  reconsider y as Element of X by A2,TARSKI:def 1;
  reconsider x as Element of X by A1;
  y=0.X by A2,TARSKI:def 1;
  then x\0.X in I by A2,Def12;
  hence thesis by BCIALG_1:2;
end;

theorem
  I is closed iff I = Class(RI,0.X)
proof
  thus I is closed implies I = Class(RI,0.X)
  proof
    assume
A1: I is closed;
    thus I c= Class(RI,0.X)
    proof
      let x be set;
      assume
A2:   x in I;
      then reconsider x as Element of I;
A3:   x` in I by A1,BCIALG_1:def 19;
A4:   0.X in {0.X} by TARSKI:def 1;
      x\0.X in I by A2,BCIALG_1:2;
      then [0.X,x] in RI by A3,Def12;
      hence thesis by A4,RELAT_1:def 13;
    end;
    thus Class(RI,0.X) c= I by Th38;
  end;
  assume
A5: I = Class(RI,0.X);
  now
    let x be Element of I;
    consider y being set such that
A6: [y,x] in RI & y in {0.X} by A5,RELAT_1:def 13;
    [0.X,x] in RI by A6,TARSKI:def 1;
    hence x` in I by Def12;
  end;
  hence thesis by BCIALG_1:def 19;
end;

theorem Th40:
  [x,y] in E implies x\y in Class(E,0.X) & y\x in Class(E,0.X)
proof
  assume
A1: [x,y] in E;
A2: 0.X in {0.X} by TARSKI:def 1;
  E is reflexive symmetric transitive&field E = the carrier of X
  by EQREL_1:16;
  then E is_symmetric_in the carrier of X &
  E is_reflexive_in the carrier of X by RELAT_2:def 9,def 11;
  then [y,x] in E & [y,y] in E&[x,x] in E by A1,RELAT_2:def 1,def 3;
  then [x\x,y\x] in E&[y\y,x\y] in E by A1,Def9;
  then [0.X,y\x] in E &[0.X,x\y] in E by BCIALG_1:def 5;
  hence thesis by A2,RELAT_1:def 13;
end;

theorem
  for A,I being Ideal of X,IA being I-congruence of X,A,
  II being I-congruence of X,I st Class(IA,0.X)=Class(II,0.X) holds IA = II
proof
  let A,I be Ideal of X,IA be I-congruence of X,A,II be I-congruence of X,I;
  assume
A1: Class(IA,0.X) = Class(II,0.X);
  let xx,yy be set;
  thus [xx,yy] in IA implies [xx,yy] in II
  proof
    assume
A2: [xx,yy] in IA;
    then consider x,y being set such that
A3: [xx,yy]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A3;
A4: y\x in II.:{0.X}&x\y in II.:{0.X} by A1,A2,A3,Th40;
    then consider z being set such that
A5: [z,y\x] in II & z in {0.X}by RELAT_1:def 13;
    [0.X,y\x] in II by A5,TARSKI:def 1;
    then y\x\0.X in I by Def12;
    then
A6: y\x in I by BCIALG_1:2;
    consider z being set such that
A7: [z,x\y] in II & z in {0.X}by A4,RELAT_1:def 13;
    [0.X,x\y] in II by A7,TARSKI:def 1;
    then x\y\0.X in I by Def12;
    then x\y in I by BCIALG_1:2;
    hence [xx,yy] in II by A3,A6,Def12;
  end;
  thus [xx,yy] in II implies [xx,yy] in IA
  proof
    assume
A8: [xx,yy] in II;
    then consider x,y being set such that
A9: [xx,yy]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A9;
A10: y\x in IA.:{0.X}&x\y in IA.:{0.X} by A1,A8,A9,Th40;
    then consider z being set such that
A11: [z,y\x] in IA & z in {0.X}by RELAT_1:def 13;
    [0.X,y\x] in IA by A11,TARSKI:def 1;
    then y\x\0.X in A by Def12;
    then
A12: y\x in A by BCIALG_1:2;
    consider z being set such that
A13: [z,x\y] in IA & z in {0.X}by A10,RELAT_1:def 13;
    [0.X,x\y] in IA by A13,TARSKI:def 1;
    then x\y\0.X in A by Def12;
    then x\y in A by BCIALG_1:2;
    hence [xx,yy] in IA by A9,A12,Def12;
  end;
end;

theorem Th42:
  [x,y] in E & u in Class(E,0.X) implies [x,(y,u)to_power k] in E
proof
  assume
A1: [x,y] in E & u in Class(E,0.X);
  then consider z being set such that
A2: [z,u] in E & z in {0.X} by RELAT_1:def 13;
A3: [0.X,u] in E by A2,TARSKI:def 1;
  defpred P[Element of NAT] means [x,(y,u)to_power $1] in E;
A4: P[0] by A1,Th1;
A5: for k be Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT;
    assume [x,(y,u) to_power k] in E;
    then [x\0.X,(y,u)to_power k\u] in E by A3,Def9;
    then [x,(y,u)to_power k\u] in E by BCIALG_1:2;
    hence [x,(y,u)to_power (k+1)] in E by Th4;
  end;
  for n holds P[n] from NAT_1:sch 1(A4,A5);
  hence thesis;
end;

theorem
  (for X,x,y holds ex i,j,m,n 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,I st I=Class(E,0.X) holds E is I-congruence of X,I
proof
  assume
A1: for X,x,y holds ex i,j,m,n st
  ((x,x\y)to_power i,y\x)to_power j =((y,y\x)to_power m,x\y)to_power n;
  let E,I;
  assume
A2: I=Class(E,0.X);
  now
    let x,y be Element of X;
    x\y in I & y\x in I implies[x,y] in E
    proof
      assume
A3:   x\y in I & y\x in I;
      then consider z being set such that
A4:   [z,y\x] in E & z in {0.X}by A2,RELAT_1:def 13;
A5:   [0.X,y\x] in E by A4,TARSKI:def 1;
      consider z being set such that
A6:   [z,x\y] in E & z in {0.X}by A2,A3,RELAT_1:def 13;
A7:   [0.X,x\y] in E by A6,TARSKI:def 1;
      consider i,j,m,n being Element of NAT such that
A8:   ((x,x\y)to_power i,y\x)to_power j
      =((y,y\x)to_power m,x\y)to_power n by A1;
A9:   E is reflexive symmetric transitive
      & field E = the carrier of X by EQREL_1:16;
A10:  E is_reflexive_in field E & E is_symmetric_in field E
      &E is_transitive_in field E by RELAT_2:def 9,def 11,def 16;
      then [x,x] in E & [y,y] in E by A9,RELAT_2:def 1;
      then
A11:  [x,(x,x\y) to_power i] in E & [y,(y,y\x) to_power m] in E by A2,A3,Th42;
A12:  [x,((x,(x\y))to_power i,y\x)to_power j] in E
      proof
        defpred P[Element of NAT] means
        [x,((x,(x\y))to_power i,y\x)to_power $1] in E;
A13:    P[0] by A11,Th1;
A14:    for k be Element of NAT st P[k] holds P[k+1]
        proof
          let k be Element of NAT;
          assume [x,((x,(x\y))to_power i,y\x)to_power k] in E;

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 [x,((x,(x\y))to_power i,y\x)to_power (k+1)] in E by Th4;
        end;
        for n holds P[n] from NAT_1:sch 1(A13,A14);
        hence thesis;
      end;
      [y,((y,(y\x))to_power m,x\y)to_power n] in E
      proof
        defpred P[Element of NAT] means
        [y,((y,(y\x))to_power m,x\y)to_power $1] in E;
A15:    P[0] by A11,Th1;
A16:    for k be Element of NAT st P[k] holds P[k+1]
        proof
          let k be Element of NAT;
          assume [y,((y,(y\x))to_power m,x\y)to_power k] in E;

then [y\0.X,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by A7,Def9;

then [y,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by BCIALG_1:2;
          hence [y,((y,(y\x))to_power m,x\y)to_power (k+1)] in E by Th4;
        end;
        for n holds P[n] from NAT_1:sch 1(A15,A16);
        hence thesis;
      end;

then [((x,(x\y))to_power i,y\x)to_power j,y] in E by A8,A9,A10,RELAT_2:def 3;
      hence [x,y] in E by A9,A10,A12,RELAT_2:def 8;
    end;
    hence [x,y] in E iff x\y in I & y\x in I by A2,Th40;
  end;
  hence thesis by Def12;
end;

theorem
  IConSet(X) c= ConSet(X)
proof
  let x be set;
  assume x in IConSet(X);
  then consider I being Ideal of X such that
A1: x is I-congruence of X,I by Def13;
  thus thesis by A1;
end;

theorem Th45:
  ConSet(X) c= LConSet(X)
proof
  let x be set;
  assume x in ConSet(X);
  then consider R being Congruence of X such that
A1: x=R;
  x is L-congruence of X by A1,Th36;
  hence thesis;
end;

theorem Th46:
  ConSet(X) c= RConSet(X)
proof
  let x be set;
  assume x in ConSet(X);
  then consider R being Congruence of X such that
A1: x=R;
  x is R-congruence of X by A1,Th36;
  hence thesis;
end;

theorem
  ConSet(X) = LConSet(X)/\RConSet(X)
proof
  thus ConSet(X) c= LConSet(X)/\RConSet(X)
  proof
    ConSet(X) c= LConSet(X)&ConSet(X) c= RConSet(X) by Th45,Th46;
    hence thesis by XBOOLE_1:19;
  end;
  thus LConSet(X)/\RConSet(X) c= ConSet(X)
  proof
    let x be set;
    assume x in LConSet(X)/\RConSet(X);
    then
A1: x in LConSet(X) & x in RConSet(X) by XBOOLE_0:def 3;
    then consider R being R-congruence of X such that
A2: x=R;
    consider L being L-congruence of X such that
A3: x=L by A1;
    x is Congruence of X by A2,A3,Th36;
    hence thesis;
  end;
end;

theorem
  (for LC holds LC is I-congruence of X,I) implies E = RI
proof
  assume
A1: for LC holds LC is I-congruence of X,I;
  E is L-congruence of X by Th36;
  then
A2: E is I-congruence of X,I by A1;
  let x1,y1 be set;
  thus [x1,y1] in E implies [x1,y1] in RI
  proof
    assume
A3: [x1,y1] in E;
    then consider x,y being set such that
A4: [x1,y1]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A4;
A5: x\y in Class(E,0.X)& y\x in Class(E,0.X) by A3,A4,Th40;
    then consider z being set such that
A6: [z,x\y] in E & z in {0.X}by RELAT_1:def 13;
    [0.X,x\y] in E by A6,TARSKI:def 1;
    then x\y\0.X in I by A2,Def12;
    then
A7: x\y in I by BCIALG_1:2;
    consider z being set such that
A8: [z,y\x] in E & z in {0.X}by A5,RELAT_1:def 13;
    [0.X,y\x] in E by A8,TARSKI:def 1;
    then y\x\0.X in I by A2,Def12;
    then y\x in I by BCIALG_1:2;
    hence thesis by A4,A7,Def12;
  end;
  thus [x1,y1] in RI implies [x1,y1] in E
  proof
    assume
A9: [x1,y1] in RI;
    then consider x,y being set such that
A10: [x1,y1]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A10;
    x\y in I & y\x in I by A9,A10,Def12;
    hence thesis by A2,A10,Def12;
  end;
end;

theorem
  (for RC holds RC is I-congruence of X,I) implies E = RI
proof
  assume
A1: for RC holds RC is I-congruence of X,I;
  E is R-congruence of X by Th36;
  then
A2: E is I-congruence of X,I by A1;
  let x1,y1 be set;
  thus [x1,y1] in E implies [x1,y1] in RI
  proof
    assume
A3: [x1,y1] in E;
    then consider x,y being set such that
A4: [x1,y1]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A4;
A5: x\y in Class(E,0.X)& y\x in Class(E,0.X) by A3,A4,Th40;
    then consider z being set such that
A6: [z,x\y] in E & z in {0.X}by RELAT_1:def 13;
    [0.X,x\y] in E by A6,TARSKI:def 1;
    then x\y\0.X in I by A2,Def12;
    then
A7: x\y in I by BCIALG_1:2;
    consider z being set such that
A8: [z,y\x] in E & z in {0.X}by A5,RELAT_1:def 13;
    [0.X,y\x] in E by A8,TARSKI:def 1;
    then y\x\0.X in I by A2,Def12;
    then y\x in I by BCIALG_1:2;
    hence thesis by A4,A7,Def12;
  end;
  thus [x1,y1] in RI implies [x1,y1] in E
  proof
    assume
A9: [x1,y1] in RI;
    then consider x,y being set such that
A10: [x1,y1]=[x,y] & x in the carrier of X &y in the carrier of X
    by RELSET_1:6;
    reconsider x,y as Element of X by A10;
    x\y in I & y\x in I by A9,A10,Def12;
    hence thesis by A2,A10,Def12;
  end;
end;

theorem
  Class(LC,0.X) is closed Ideal of X
proof
A1: [0.X,0.X] in LC by EQREL_1:11;
  Class(LC,0.X) is Ideal of X
  proof
A2: 0.X in Class(LC,0.X) by A1,EQREL_1:26;
    now
      let x,y be Element of X;
      assume x\y in Class(LC,0.X) & y in Class(LC,0.X);
      then
A3:   [0.X,x\y] in LC & [0.X,y] in LC by EQREL_1:26;
      then [x\0.X,x\y] in LC by Def10;
      then [x,x\y] in LC by BCIALG_1:2;
      then [x\y,x] in LC by EQREL_1:12;
      then [0.X,x] in LC by A3,EQREL_1:13;
      hence x in Class(LC,0.X)by EQREL_1:26;
    end;
    hence thesis by A2,BCIALG_1:def 18;
  end;
  then reconsider Rx=Class(LC,0.X) as Ideal of X;
  Rx is closed
  proof
    now
      let x be Element of Rx;
      [0.X,x] in LC by EQREL_1:26;
      then [(0.X)`,x`] in LC by Def10;
      then [0.X,x`] in LC by BCIALG_1:def 5;
      hence x` in Class(LC,0.X) by EQREL_1:26;
    end;
    hence thesis by BCIALG_1:def 19;
  end;
  hence thesis;
end;

::::::::::::::::::::::::::::  Quotient Algebras  :::::::::::

reserve E for Congruence of X;
reserve RI for I-congruence of X,I;

registration
  let X,E;
  cluster Class E -> non empty;
  coherence
  proof
    Class(E,0.X) in Class E by EQREL_1:def 5;
    hence thesis;
  end;
end;

definition
  let X,E;
  func EqClaOp E -> BinOp of Class E means
  :Def17:
  for W1,W2 being Element of Class(E)
  for x,y st W1=Class(E,x) & W2=Class(E,y) holds it.(W1,W2)=Class(E,x\y);
  existence
  proof
    defpred P[Element of Class E,Element of Class E,set] means
    for x,y st $1 =Class(E,x) & $2 = Class(E,y) holds $3 = Class(E,x\y);
A1: for W1,W2 being Element of Class E
    ex V being Element of Class E st P[W1,W2,V]
    proof
      let W1,W2 be Element of Class E;
      consider x1 being set such that
A2:   x1 in the carrier of X & W1 = Class(E,x1) by EQREL_1:def 5;
      consider y1 being set such that
A3:   y1 in the carrier of X & W2 = Class(E,y1) by EQREL_1:def 5;
      reconsider x1,y1 as Element of X by A2,A3;
      reconsider C = Class(E,x1\y1) as Element of Class E by EQREL_1:def 5;
      take C;
      now
        let x,y;
        assume W1=Class(E,x)&W2=Class(E,y);
        then x in Class(E,x1)&y in Class(E,y1) by A2,A3,EQREL_1:31;
        then [x1,x] in E &[y1,y] in E by EQREL_1:26;
        then [x1\y1,x\y] in E by Def9;
        then x\y in Class(E,x1\y1) by EQREL_1:26;
        hence C = Class(E,x\y) by EQREL_1:31;
      end;
      hence thesis;
    end;
    thus ex B being BinOp of Class E st
    for W1,W2 being Element of Class E holds
    P[W1,W2,B.(W1,W2)] from BINOP_1:sch 3(A1);
  end;
  uniqueness
  proof
    let o1,o2 be BinOp of Class E;
    assume
A4: for W1,W2 being Element of Class E
    for x,y st W1=Class(E,x)&W2=Class(E,y)holds o1.(W1,W2)=Class(E,x\y);
    assume
A5: for W1,W2 being Element of Class E
    for x,y st W1=Class(E,x)&W2=Class(E,y)holds o2.(W1,W2)=Class(E,x\y);
    now
      let W1,W2 be Element of Class(E);
      consider x being set such that
A6:   x in the carrier of X & W1 = Class(E,x) by EQREL_1:def 5;
      consider y being set such that
A7:   y in the carrier of X & W2 = Class(E,y) by EQREL_1:def 5;
      reconsider x,y as Element of X by A6,A7;
      o1.(W1,W2)=Class(E,x\y) by A4,A6,A7;
      hence o1.(W1,W2) = o2.(W1,W2) by A5,A6,A7;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let X,E;
  func zeroEqC(E) -> Element of Class E equals

  Class(E,0.X);
  coherence by EQREL_1:def 5;
end;

::Quotient Algebras

definition
  let X,E;
  func X./.E -> BCIStr_0 equals

  BCIStr_0(#Class E,EqClaOp E,zeroEqC(E)#);
  coherence;
end;

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

reserve W1,W2,W3 for Element of Class E;

definition
  let X,E,W1,W2;
  func W1\W2 -> Element of Class E equals

  (EqClaOp E).(W1,W2);
  coherence;
end;

theorem Th51:
  X./.RI is BCI-algebra
proof
  reconsider IT = X./.RI as non empty BCIStr_0;
A1: IT is_B
  proof
    now
      let w1,w2,w3 be Element of IT;
A2:   w1 in the carrier of IT&w2 in the carrier of IT&w3 in the carrier of IT;
      then consider x1 being set such that
A3:   x1 in the carrier of X & w1 = Class(RI,x1) by EQREL_1:def 5;
      consider y1 being set such that
A4:   y1 in the carrier of X & w2 = Class(RI,y1) by A2,EQREL_1:def 5;
      consider z1 being set such that
A5:   z1 in the carrier of X & w3 = Class(RI,z1) by A2,EQREL_1:def 5;
      reconsider x1,y1,z1 as Element of X by A3,A4,A5;
A6:   w1\w2=Class(RI,x1\y1)&w3\w2=Class(RI,z1\y1)&
      w1\w3=Class(RI,x1\z1) by A3,A4,A5,Def17;
      then (w1\w2)\(w3\w2)=Class(RI,(x1\y1)\(z1\y1)) by Def17;

then (w1\w2)\(w3\w2)\(w1\w3)=Class(RI,(x1\y1)\(z1\y1)\(x1\z1)) by A6,Def17;
      hence ((w1\w2)\(w3\w2))\(w1\w3)=0.IT by BCIALG_1:def 3;
    end;
    hence thesis by BCIALG_1:def 3;
  end;
A7: IT is_C
  proof
    now
      let w1,w2,w3 be Element of IT;
A8:   w1 in the carrier of IT&w2 in the carrier of IT&w3 in the carrier of IT;
      then consider x1 being set such that
A9:   x1 in the carrier of X & w1 = Class(RI,x1) by EQREL_1:def 5;
      consider y1 being set such that
A10:  y1 in the carrier of X & w2 = Class(RI,y1) by A8,EQREL_1:def 5;
      consider z1 being set such that
A11:  z1 in the carrier of X & w3 = Class(RI,z1) by A8,EQREL_1:def 5;
      reconsider x1,y1,z1 as Element of X by A9,A10,A11;
      w1\w2=Class(RI,x1\y1)& w1\w3=Class(RI,x1\z1) by A9,A10,A11,Def17;
      then (w1\w2)\w3=Class(RI,(x1\y1)\z1)
      &(w1\w3)\w2=Class(RI,x1\z1\y1) by A10,A11,Def17;
      then ((w1\w2)\w3)\((w1\w3)\w2)=Class(RI,(x1\y1)\z1\(x1\z1\y1)) by Def17;
      hence ((w1\w2)\w3)\((w1\w3)\w2)=0.IT by BCIALG_1:def 4;
    end;
    hence thesis by BCIALG_1:def 4;
  end;
A12: IT is_I
  proof
    now
      let w1 be Element of IT;
      w1 in the carrier of IT;
      then consider x1 being set such that
A13:  x1 in the carrier of X & w1 = Class(RI,x1) by EQREL_1:def 5;
      reconsider x1 as Element of X by A13;
      w1\w1=Class(RI,x1\x1) by A13,Def17;
      hence w1\w1 = 0.IT by BCIALG_1:def 5;
    end;
    hence thesis by BCIALG_1:def 5;
  end;
  IT is_BCI-4
  proof
    now
      let w1,w2 be Element of IT;
      assume
A14:  w1\w2=0.IT & w2\w1=0.IT;
A15:  w1 in the carrier of IT&w2 in the carrier of IT;
      then consider x1 being set such that
A16:  x1 in the carrier of X & w1 = Class(RI,x1) by EQREL_1:def 5;
      consider y1 being set such that
A17:  y1 in the carrier of X & w2 = Class(RI,y1) by A15,EQREL_1:def 5;
      reconsider x1,y1 as Element of X by A16,A17;
      w1\w2=Class(RI,x1\y1)& w2\w1=Class(RI,y1\x1) by A16,A17,Def17;
      then 0.X in Class(RI,x1\y1) & 0.X in Class(RI,y1\x1) by A14,EQREL_1:31;
      then [x1\y1,0.X] in RI & [y1\x1,0.X] in RI by EQREL_1:26;
      then x1\y1\0.X in I & y1\x1\0.X in I by Def12;
      then x1\y1 in I & y1\x1 in I by BCIALG_1:2;
      then [x1,y1] in RI by Def12;
      hence w1=w2 by A16,A17,EQREL_1:44;
    end;
    hence thesis by BCIALG_1:def 7;
  end;
  hence thesis by A1,A7,A12;
end;

registration
  let X,I,RI;
  cluster X./.RI -> strict being_B being_C being_I being_BCI-4;
  coherence by Th51;
end;

theorem
  for X,I st I = BCK-part(X) holds for RI being I-congruence of X,I
  holds X./.RI is p-Semisimple BCI-algebra
proof
  let X,I;
  assume
A1: I = BCK-part(X);
  let RI be I-congruence of X,I;
  set IT = X./.RI;
  for w1 being Element of IT holds (w1`)` = w1
  proof
    let w1 be Element of IT;
    w1 in the carrier of IT;
    then consider x1 being set such that
A2: x1 in the carrier of X & w1 = Class(RI,x1) by EQREL_1:def 5;
    reconsider x1 as Element of X by A2;
    w1`= Class(RI,x1`) by A2,Def17;
    then
A3: w1``=Class(RI,x1``) by Def17;
    0.X in I by BCIALG_1:def 18;
    then
A4: (x1`)`\x1 in I by BCIALG_1:1;
    x1\((x1`)`) is positive Element of X by Th28;
    then 0.X <= x1\(x1``) by Def2;
    then x1\(x1``) in I by A1;
    then [x1``,x1] in RI by A4,Def12;
    hence thesis by A2,A3,EQREL_1:44;
  end;
  hence thesis by BCIALG_1:54;
end;