:: Several Classes of {BCI}-algebras and Their Properties
::  by Yuzhong Ding
::
:: Received February 23, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies BINOP_1, BCIALG_1, BOOLE, FILTER_0, MIDSP_1, RLVECT_1, UNIALG_2,
      VECTSP_2, WAYBEL15, FILTER_2, PRE_TOPC, FUNCT_1, RELAT_1, COLLSP,
      SUBSET_1, REALSET1, STRUCT_0;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, BINOP_1, FUNCT_5, REALSET1,
      STRUCT_0, RELAT_1;
 constructors BINOP_1, REALSET1, MIDSP_1, FUNCT_5;
 registrations XBOOLE_0, RELAT_1, STRUCT_0, REALSET1;
 requirements SUBSET, BOOLE;
 definitions REALSET1, TARSKI, XBOOLE_0, STRUCT_0;
 theorems TARSKI, ZFMISC_1, XBOOLE_0, STRUCT_0, FUNCT_2, RELAT_1, CARD_1;

begin :: The Basics of General Theory of BCI-algebra

definition
  struct (1-sorted) BCIStr (# carrier -> set,
    InternalDiff -> BinOp of the carrier #);
end;

registration
  cluster non empty strict BCIStr;
  existence
  proof
    consider A being non empty set, m being BinOp of A;
    take BCIStr(#A,m#);
    thus the carrier of BCIStr(#A,m#) is non empty;
    thus thesis;
  end;
end;

definition
  let A be BCIStr;
  let x,y be Element of A;
  func x \ y -> Element of A equals

  (the InternalDiff of A).(x,y);
  coherence;
end;

definition
  struct (BCIStr,ZeroStr) BCIStr_0 (# carrier -> set,
    InternalDiff -> BinOp of the carrier, ZeroF -> Element of the carrier #);
end;

registration
  cluster non empty strict BCIStr_0;
  existence
  proof
    consider A being non empty set, m being BinOp of A, u being Element of A;
    take BCIStr_0(#A,m,u#);
    thus the carrier of BCIStr_0(#A,m,u#) is non empty;
    thus thesis;
  end;
end;

definition
  let IT be non empty BCIStr_0, x be Element of IT;
  func x` -> Element of IT equals

  0.IT\x;
  coherence;
end;

definition
  let IT be non empty BCIStr_0;
  attr IT is being_B means
  :Def3:
  for x,y,z being Element of IT holds ((x\y)\(z\y))\(x\z)=0.IT;
  attr IT is being_C means
  :Def4:
  for x,y,z being Element of IT holds ((x\y)\z)\((x\z)\y)=0.IT;
  attr IT is being_I means
  :Def5:
  for x being Element of IT holds x\x=0.IT;
  attr IT is being_K means
  :Def6:
  for x,y being Element of IT holds (x\y)\x=0.IT;
  attr IT is being_BCI-4 means
  :Def7:
  for x,y being Element of IT holds (x\y=0.IT&y\x=0.IT implies x = y);
  attr IT is being_BCK-5 means
  :Def8:
  for x being Element of IT holds x`=0.IT;
end;

notation
  let IT be non empty BCIStr_0;
  synonym IT is_B for IT is being_B;
  synonym IT is_C for IT is being_C;
  synonym IT is_I for IT is being_I;
  synonym IT is_K for IT is being_K;
  synonym IT is_BCI-4 for IT is being_BCI-4;
  synonym IT is_BCK-5 for IT is being_BCK-5;
end;

definition
  func BCI-EXAMPLE -> BCIStr_0 equals

  BCIStr_0 (# 1, op2, op0 #);
  coherence;
end;

registration
  cluster BCI-EXAMPLE -> strict non empty trivial;
  coherence by CARD_1:87;
end;

registration
  cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5;
  coherence
  proof
    thus BCI-EXAMPLE is_B
    proof
      let x,y,z be Element of BCI-EXAMPLE;
      thus thesis by STRUCT_0:def 10;
    end;
    thus BCI-EXAMPLE is_C
    proof
      let x,y,z be Element of BCI-EXAMPLE;
      thus thesis by STRUCT_0:def 10;
    end;
    thus BCI-EXAMPLE is_I
    proof
      let x be Element of BCI-EXAMPLE;
      thus thesis by STRUCT_0:def 10;
    end;
    thus BCI-EXAMPLE is_BCI-4
    proof
      let x,y be Element of BCI-EXAMPLE;
      thus thesis by STRUCT_0:def 10;
    end;
    for x being Element of BCI-EXAMPLE holds x` = 0.BCI-EXAMPLE
    by STRUCT_0:def 10;
    hence thesis by Def8;
  end;
end;

registration
  cluster strict being_B being_C being_I being_BCI-4 being_BCK-5
    (non empty BCIStr_0);
  existence
  proof
    take BCI-EXAMPLE;
    thus thesis;
  end;
end;

definition
  mode BCI-algebra is being_B being_C being_I being_BCI-4
    (non empty BCIStr_0);
end;

definition
  mode BCK-algebra is being_BCK-5 BCI-algebra;
end;

definition
  let X be BCI-algebra;
  mode SubAlgebra of X -> BCI-algebra means
    :Def10:
    0.it = 0.X &
    the carrier of it c= the carrier of X & the InternalDiff of it
    = (the InternalDiff of X)||the carrier of it;
  existence
  proof
    take X;
    dom(the InternalDiff of X) = [:the carrier of X,the carrier of X:]
    by FUNCT_2:def 1;
    hence thesis by RELAT_1:97;
  end;
end;

::T1.1.11

theorem Th1:
  for X being non empty BCIStr_0 holds (X is BCI-algebra iff
  (X is_I & X is_BCI-4 &for x,y,z being Element of X holds
  ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X ))
proof
  let X be non empty BCIStr_0;
  thus X is BCI-algebra implies
  (X is_I & X is_BCI-4 &for x,y,z being Element of X holds
  ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X )
  proof
    assume
A1: X is BCI-algebra;
    now
      let x,y,z be Element of X;
A2:   ((x\y)\(z\y))\(x\z)=0.X by A1,Def3;
A3:   for x,y,z being Element of X holds (x\y)\z = (x\z)\y
      proof
        let x,y,z be Element of X;
        ((x\y)\z)\((x\z)\y)=0.X &((x\z)\y)\((x\y)\z)=0.X by A1,Def4;
        hence (x\y)\z = (x\z)\y by A1,Def7;
      end;
      then (x\(x\y))\y=(x\y)\(x\y);
      hence ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X & x\x = 0.X &
      (x\y = 0.X & y\x = 0.X implies x = y) by A1,A2,A3,Def5,Def7;
    end;
    hence thesis by A1;
  end;
  assume
A4: (X is_I & X is_BCI-4 &for x,y,z being Element of X holds
  ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X );
A5: for x being Element of X st x\0.X=0.X holds x=0.X
  proof
    let x be Element of X;
    assume
A6: x\0.X =0.X;
    then x` = (x \ (x\x)) \ x by A4,Def5
      .= 0.X by A4;
    hence thesis by A4,A6,Def7;
  end;
A7: for x being Element of X holds x \ 0.X = x
  proof
    let x be Element of X;
A8: 0.X = (x\(x\x))\x by A4
      .= (x\0.X)\x by A4,Def5;
    (x\(x\0.X))\0.X = 0.X by A4;
    then x\(x\0.X) = 0.X by A5;
    hence thesis by A4,A8,Def7;
  end;
A9: for x,y,z being Element of X st x\y=0.X & y\z=0.X holds x\z=0.X
  proof
    let x,y,z be Element of X;
    assume
A10: x\y=0.X & y\z=0.X;
    ((x\z)\(x\y))\(y\z)=0.X by A4;
    then (x\z)\(x\y)=0.X by A7,A10;
    hence thesis by A7,A10;
  end;
A11: for x,y,z being Element of X st
  x\y=0.X holds (x\z)\(y\z)=0.X&(z\y)\(z\x)=0.X
  proof
    let x,y,z be Element of X;
    assume
A12: x\y=0.X;
A13: ((z\y)\(z\x))\(x\y)=0.X by A4;
    ((x\z)\(x\y))\(y\z)=0.X by A4;
    hence thesis by A7,A12,A13;
  end;
A14: for x,y,z being Element of X holds ((x\y)\(z\y))\(x\z) = 0.X
  proof
    let x,y,z be Element of X;
    ((x\y)\(x\z))\(z\y) = 0.X by A4;
    then ((x\y)\(z\y))\((x\y)\((x\y)\(x\z))) = 0.X by A11;
    then (((x\y)\(z\y))\(x\z))\(((x\y)\((x\y)\(x\z)))\(x\z)) = 0.X by A11;
    then (((x\y)\(z\y))\(x\z))\ 0.X = 0.X by A4;
    hence thesis by A5;
  end;
  for x,y,z being Element of X holds ((x\y)\z)\((x\z)\y) = 0.X
  proof
    let x,y,z be Element of X;
    (((x\y)\z)\((x\y)\(x\(x\z))))\((x\(x\z))\z)=0.X by A4;
    then (((x\y)\z)\((x\y)\(x\(x\z))))\0.X=0.X by A4;
    then
A15: ((x\y)\z)\((x\y)\(x\(x\z)))=0.X by A5;
    ((x\y)\(x\(x\z)))\((x\z)\y) = 0.X by A4;
    hence thesis by A9,A15;
  end;
  hence thesis by A4,A14,Def3,Def4;
end;

definition
  let IT be non empty BCIStr_0;
  let x,y be Element of IT;
  pred x <= y means
  :Def11:
  x \ y = 0.IT;
end;

reserve X for BCI-algebra;
reserve x,y,z,u,v,a,b for Element of X;
reserve IT for non empty Subset of X;

Lm1: x\0.X = 0.X implies x = 0.X
proof
  assume
A1: x\0.X =0.X;
  then x` = (x \ (x\x)) \ x by Def5
    .= 0.X by Th1;
  hence thesis by A1,Def7;
end;

theorem Th2:
  x \ 0.X = x
proof
A1: 0.X = (x\(x\x))\x by Th1
    .= (x\0.X)\x by Def5;
  (x\(x\0.X))\0.X = 0.X by Th1;
  then x\(x\0.X) = 0.X by Lm1;
  hence thesis by A1,Def7;
end;

theorem Th3:
  x\y=0.X & y\z=0.X implies x\z=0.X
proof
  assume
A1: x\y=0.X & y\z=0.X;
  ((x\z)\(x\y))\(y\z)=0.X by Th1;
  then (x\z)\(x\y)=0.X by A1,Th2;
  hence thesis by A1,Th2;
end;

theorem Th4:
  x\y=0.X implies (x\z)\(y\z)=0.X & (z\y)\(z\x)=0.X
proof
  assume
A1: x\y=0.X;
A2: ((z\y)\(z\x))\(x\y)=0.X by Th1;
  ((x\z)\(x\y))\(y\z)=0.X by Th1;
  hence thesis by A1,A2,Th2;
end;

theorem
  x <= y implies x\z <= y\z & z\y <= z\x
proof
  assume x <= y;
  then x\y = 0.X by Def11;
  then (x\z)\(y\z)=0.X&(z\y)\(z\x)=0.X by Th4;
  hence thesis by Def11;
end;

theorem
  x\y=0.X implies (y\x)` = 0.X
proof
  assume x\y = 0.X;
  then (x\x)\(y\x) = 0.X by Th4;
  hence thesis by Def5;
end;

theorem Th7:
  (x\y)\z = (x\z)\y
proof
  (x\(x\z))\z = 0.X by Th1;
  then
A1: ((x\y)\z)\((x\y)\(x\(x\z)))=0.X by Th4;
  ((x\y)\(x\(x\z)))\((x\z)\y) = 0.X by Th1;
  then
A2: ((x\y)\z)\((x\z)\y) = 0.X by A1,Th3;
  (x\(x\y))\y = 0.X by Th1;
  then
A3: ((x\z)\y)\((x\z)\(x\(x\y)))=0.X by Th4;
  ((x\z)\(x\(x\y)))\((x\y)\z) = 0.X by Th1;
  then ((x\z)\y)\((x\y)\z) = 0.X by A3,Th3;
  hence thesis by A2,Def7;
end;

theorem Th8:
  x\(x\(x\y)) = x\y
proof
A1: (x\(x\(x\y)))\(x\y) = 0.X by Th1;
  (x\y)\(x\(x\(x\y)))\((x\(x\y))\y) = 0.X by Th1;
  then (x\y)\(x\(x\(x\y)))\0.X = 0.X by Th1;
  then (x\y)\(x\(x\(x\y))) = 0.X by Th2;
  hence thesis by A1,Def7;
end;

theorem Th9:
  (x\y)` = x`\y`
proof
  x`\y`= ((((x\y)\(x\y))\x)\y`) by Def5
    .= ((((x\y)\x)\(x\y))\y`) by Th7
    .= ((((x\x)\y)\(x\y))\y`) by Th7
    .= ((y`\(x\y))\y`) by Def5
    .= (y`\y`)\(x\y) by Th7;
  hence thesis by Def5;
end;

theorem Th10:
  ((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X
proof
  ((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))
  =((x\(x\y))\(x\(x\(y\(y\x)))))\(y\x) by Th7
    .=((x\(x\(x\(y\(y\x)))))\(x\y))\(y\x) by Th7
    .=((x\(y\(y\x)))\(x\y))\(y\x) by Th8
    .=((x\(y\(y\x)))\(x\y))\(y\(y\(y\x))) by Th8;
  hence thesis by Th1;
end;

theorem ::T1.1.6
  for X being non empty BCIStr_0 holds (X is BCI-algebra iff (X is_BCI-4 &
  for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X = x ))
proof
  let X be non empty BCIStr_0;
  thus X is BCI-algebra implies (X is_BCI-4 &
  for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X &
  x\0.X = x ) by Th1,Th2;
  thus (X is_BCI-4 & for x,y,z being Element of X holds
  ((x\y)\(x\z))\(z\y)=0.X & x\0.X = x )implies X is BCI-algebra
  proof
    assume
A1: X is_BCI-4 & for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X &
    x\0.X = x;
A2: X is_I
    proof
      let x be Element of X;
      x\x=(x\x)\0.X by A1;
      then x\x=((x\0.X)\x)\0.X by A1;
      then x\x=((x\0.X)\(x\0.X))\0.X by A1;
      then x\x=((x\0.X)\(x\0.X))\(0.X)` by A1;
      hence thesis by A1;
    end;
    now
      let x,y,z be Element of X;
      ((x\0.X)\(x\y))\(y\0.X)=0.X by A1;
      then (x\(x\y))\(y\0.X)=0.X by A1;
      hence ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X by A1;
    end;
    hence thesis by A1,A2,Th1;
  end;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x))
  implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x);
  for z being Element of X holds z` = 0.X
  proof
    let z be Element of X;
    z`` = z \ (z \ 0.X) by A1;
    then z`` = z \ z by Th2;
    then z`` \ z = z` by Def5;
    hence thesis by Th1;
  end;
  hence thesis by Def8;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y)
  implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y;
  for z being Element of X holds z` = 0.X
  proof
    let z be Element of X;
    z`\(z` \ z) =z`\z` by A1;
    then z`\(z` \ z) =0.X by Def5;
    hence thesis by Th1;
  end;
  hence thesis by Def8;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x)
  implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x;
  for z being Element of X holds z` = 0.X
  proof
    let z be Element of X;
    (z \ 0.X )` = 0.X by A1;
    hence thesis by Th2;
  end;
  hence thesis by Def8;
end;

theorem
  (for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\(y\z)
  ) implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\(y\z);
  for s being Element of X holds s` = 0.X
  proof
    let s be Element of X;
    s` \ s=s` \ (s \ s) by A1;
    then s` \ s=s` \ 0.X by Def5;
    then s`\(s` \ s) =s`\s` by Th2;
    then s`\(s` \ s) =0.X by Def5;
    hence thesis by Th1;
  end;
  hence thesis by Def8;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y)
  implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y;
  for s being Element of X holds s` = 0.X
  proof
    let s be Element of X;
    s` \ (s \ 0.X ) = s` by A1;
    then s`\(s` \ s) =s`\s` by Th2;
    then s`\(s` \ s) =0.X by Def5;
    hence thesis by Th1;
  end;
  hence thesis by Def8;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds
  (x\y)\((x\y)\(y\x))=0.X) implies X is BCK-algebra
proof
  assume
A1: for X being BCI-algebra,x,y being Element of X holds
  (x\y)\((x\y)\(y\x))=0.X;
  for s being Element of X holds s` = 0.X
  proof
    let s be Element of X;
    s`\(s`\(s\0.X))=0.X by A1;
    then (s`\(s`\s))\s=s` by Th2;
    hence thesis by Th1;
  end;
  hence thesis by Def8;
end;

theorem
  for X being BCI-algebra holds X is_K iff X is BCK-algebra
proof
  let X be BCI-algebra;
  thus X is_K implies X is BCK-algebra
  proof
    assume
A1: X is_K;
    X is_BCK-5
    proof
      now
        let s be Element of X;
        s`\0.X = 0.X by A1,Def6;
        hence s` = 0.X by Th2;
      end;
      hence thesis by Def8;
    end;
    hence thesis;
  end;
  assume
A2: X is BCK-algebra;
  let x,y be Element of X;
  y` = 0.X by A2,Def8;
  then (x\y)\(x\0.X) = 0.X by Th4;
  hence thesis by Th2;
end;

definition
  let X be BCI-algebra; ::P4 1.3 atom BranchV
  func BCK-part(X) -> non empty Subset of X equals
  {x where x is Element of X:0.X<=x};
  coherence
  proof
    set Y={x where x is Element of X:0.X<=x};
    (0.X)`=0.X by Def5;
    then 0.X <= 0.X by Def11;
    then
A1: 0.X in Y;
    now
      let y be set;
      assume y in Y;
      then ex x being Element of X st y=x & 0.X<=x;
      hence y in the carrier of X;
    end;
    hence thesis by A1,TARSKI:def 3;
  end;
end;

theorem Th19:
  0.X in BCK-part(X)
proof
  (0.X)`=0.X by Def5;
  then 0.X <= 0.X by Def11;
  hence thesis;
end;

theorem
  for x,y being Element of BCK-part(X) holds x\y in BCK-part(X)
proof
  let x,y be Element of BCK-part(X);
A1: x in {x1 where x1 is Element of X:0.X<=x1} &
  y in {y1 where y1 is Element of X:0.X<=y1};
  then consider x1 being Element of X such that
A2: x=x1 & 0.X<= x1;
  consider y1 being Element of X such that
A3: y=y1&0.X<=y1 by A1;
  (x\y)`=x`\y` by Th9;
  then (x\y)`=(y`)` by A2,Def11;
  then (x\y)`=(0.X)` by A3,Def11;
  then (x\y)`=0.X by Def5;
  then 0.X <= x\y by Def11;
  hence thesis;
end;

theorem
  for x being Element of X,y being Element of BCK-part(X) holds x\y <= x
proof
  let x be Element of X,y be Element of BCK-part(X);
  y in {y1 where y1 is Element of X:0.X<=y1};
  then consider y1 being Element of X such that
A1: y=y1&0.X<=y1;
  y`=0.X by A1,Def11;
  then (x\x)\y=0.X by Def5;
  then (x\y)\x=0.X by Th7;
  hence x\y <= x by Def11;
end;

theorem Th22:
  X is SubAlgebra of X
proof
A1: the carrier of X c= the carrier of X & 0.X = 0.X;
  dom(the InternalDiff of X) = [:the carrier of X,the carrier of X:]
  by FUNCT_2:def 1;
  then the InternalDiff of X =(the InternalDiff of X)||the carrier of X
  by RELAT_1:97;
  hence thesis by A1,Def10;
end;

definition
  let X be BCI-algebra,IT be SubAlgebra of X;
  attr IT is proper means
  :Def13:
  IT <> X;
end;

registration
  let X;
  cluster non proper SubAlgebra of X;
  existence
  proof
    take X;
    X is SubAlgebra of X by Th22;
    hence thesis by Def13;
  end;
end;

definition
  let X be BCI-algebra,IT be Element of X;
  attr IT is atom means
  :Def14:
  for z being Element of X holds z\IT=0.X implies z=IT;
end;

definition
  let X be BCI-algebra;
  func AtomSet(X) -> non empty Subset of X equals
  {x where x is Element of X:x is atom};
  coherence
  proof
    set Y={x where x is Element of X:x is atom};
    for z being Element of X st z\0.X=0.X holds z=0.X by Th2;
    then 0.X is atom by Def14;
    then
A1: 0.X in Y;
    now
      let y be set;
      assume y in Y;
      then consider x being Element of X such that
A2:   y=x & x is atom;
      thus y in the carrier of X by A2;
    end;
    hence thesis by A1,TARSKI:def 3;
  end;
end;

theorem Th23:
  0.X in AtomSet(X)
proof
  for z being Element of X st z\0.X=0.X holds z=0.X by Th2;
  then 0.X is atom by Def14;
  hence thesis;
end;

theorem Th24:
  for x being Element of X holds x in AtomSet(X) iff
  for z being Element of X holds z\(z\x)=x
proof
  let x be Element of X;
  thus x in AtomSet(X) implies for z being Element of X holds z\(z\x)=x
  proof
    assume
A1: x in AtomSet(X);
    let z be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    hence (z\(z\x))=x by A2,Def14;
  end;
  assume
A3: for z being Element of X holds z\(z\x)=x;
  now
    let z be Element of X;
    assume z\x=0.X;
    then z\0.X=x by A3;
    hence z=x by Th2;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem
  for x being Element of X holds x in AtomSet(X) iff
  for u,z being Element of X holds (z\u)\(z\x)=x\u
proof
  let x be Element of X;
  thus x in AtomSet(X) implies
  for u,z being Element of X holds (z\u)\(z\x)=x\u
  proof
    assume
A1: x in AtomSet(X);
    let u,z be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    then (z\(z\x))=x by A2,Def14;
    hence (z\u)\(z\x)=x\u by Th7;
  end;
  assume
A3: for u,z being Element of X holds (z\u)\(z\x)=x\u;
  now
    let z be Element of X;
    assume z\x=0.X;
    then (z\0.X)\0.X=x\0.X by A3;
    then (z\0.X)\0.X=x by Th2;
    then z\0.X=x by Th2;
    hence z=x by Th2;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem
  for x being Element of X holds x in AtomSet(X) iff
  for y,z being Element of X holds x\(z\y)<=y\(z\x)
proof
  let x be Element of X;
  thus x in AtomSet(X)
  implies for y,z being Element of X holds x\(z\y)<=y\(z\x)
  proof
    assume
A1: x in AtomSet(X);
    let y,z be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    then (x\(z\y))\(y\(z\x))= ((z\(z\x))\(z\y))\(y\(z\x)) by A2,Def14;
    then (x\(z\y))\(y\(z\x))= ((z\(z\y))\(z\x))\(y\(z\x))by Th7;
    then (x\(z\y))\(y\(z\x))= ((z\(z\y))\(z\x))\(y\(z\x))\0.X by Th2;
    then (x\(z\y))\(y\(z\x))=((z\(z\y))\(z\x))\(y\(z\x))\((z\(z\y))\y) by Th1;
    then (x\(z\y))\(y\(z\x))=0.X by Def3;
    hence x\(z\y) <= y\(z\x) by Def11;
  end;
  assume
A3: for y,z being Element of X holds x\(z\y)<=y\(z\x);
  now
    let z be Element of X;
    assume
A4: z\x=0.X;
    (x\(z\0.X)) <= (z\x)` by A3;
    then (x\(z\0.X))\(0.X)`=0.X by A4,Def11;
    then (x\(z\0.X))\0.X = 0.X by Th2;
    then x\(z\0.X) = 0.X by Th2;
    then x\z = 0.X by Th2;
    hence z=x by A4,Def7;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem
  for x being Element of X holds x in AtomSet(X) iff
  for y,z,u being Element of X holds (x\u)\(z\y)<=(y\u)\(z\x)
proof
  let x be Element of X;
  thus x in AtomSet(X) implies
  for y,z,u being Element of X holds (x\u)\(z\y)<=(y\u)\(z\x)
  proof
    assume
A1: x in AtomSet(X);
    let y,z,u be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    then ((x\u)\(z\y))\((y\u)\(z\x))=(((z\(z\x))\u)\(z\y))\((y\u)\(z\x))
    by A2,Def14;
    then ((x\u)\(z\y))\((y\u)\(z\x))=(((z\u)\(z\x))\(z\y))\((y\u)\(z\x))by Th7;
    then ((x\u)\(z\y))\((y\u)\(z\x))=(((z\u)\(z\y))\(z\x))\((y\u)\(z\x))by Th7
      .=((((z\u)\(z\y))\(z\x))\((y\u)\(z\x)))\0.X by Th2;
    then ((x\u)\(z\y))\((y\u)\(z\x))
    =((((z\u)\(z\y))\(z\x))\((y\u)\(z\x)))\(((z\u)\(z\y))\(y\u)) by Th1;
    then ((x\u)\(z\y))\((y\u)\(z\x))=0.X by Def3;
    hence (x\u)\(z\y) <= (y\u)\(z\x) by Def11;
  end;
  assume
A3: for y,z,u being Element of X holds (x\u)\(z\y)<=(y\u)\(z\x);
  now
    let z be Element of X;
    assume
A4: z\x=0.X;
    ((x\0.X)\(z\0.X)) <= ((0.X)`\(z\x)) by A3;
    then (((x\0.X)\(z\0.X)))\(((0.X)`\0.X))=0.X by A4,Def11;
    then (((x\0.X)\(z\0.X)))\(0.X)`=0.X by Th2;
    then (((x\0.X)\(z\0.X)))\0.X=0.X by Th2;
    then (x\0.X)\(z\0.X)=0.X by Th2;
    then (x\0.X)\z=0.X by Th2;
    then x\z = 0.X by Th2;
    hence z=x by A4,Def7;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem Th28:
  for x being Element of X holds x in AtomSet(X) iff
  for z being Element of X holds z`\x`=x\z
proof
  let x be Element of X;
  thus x in AtomSet(X) implies for z being Element of X holds z`\x`=x\z
  proof
    assume
A1: x in AtomSet(X);
    let z be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    then (z\(z\x))=x by A2,Def14;
    then x\z=(z\z)\(z\x) by Th7;
    then x\z=(z\x)` by Def5;
    hence z`\x`=x\z by Th9;
  end;
  assume
A3: for z being Element of X holds z`\x`=x\z;
  now
    let z be Element of X;
    assume
A4: z\x=0.X;
    then (z\x)`=0.X by Def5;
    then z`\x`=0.X by Th9;
    then x\z = 0.X by A3;
    hence z=x by A4,Def7;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem Th29:
  for x being Element of X holds x in AtomSet(X) iff x``=x
proof
  let x be Element of X;
  thus x in AtomSet(X) implies (x`)`=x
  proof
    assume x in AtomSet(X);
    then (0.X)`\x`= x \ 0.X by Th28;
    then (0.X)`\(x`)=x by Th2;
    hence (x`)`=x by Def5;
  end;
  assume
A1: x``=x;
  now
    let z be Element of X;
    assume
A2: z\x=0.X;
    then ((z\x)\(x`))\(z\0.X)=x\z by A1,Th2;
    then 0.X=x\z by Def3;
    hence z=x by A2,Def7;
  end;
  then x is atom by Def14;
  hence thesis;
end;

theorem Th30:
  for x being Element of X holds x in AtomSet(X) iff
  for z being Element of X holds (z\x)`=x\z
proof
  let x be Element of X;
  (for z being Element of X holds (z\x)`=x\z) iff
  (for z being Element of X holds z`\x`=x\z)
  proof
    thus (for z being Element of X holds (z\x)`=x\z) implies
    (for z being Element of X holds z`\x`=x\z)
    proof
      assume
A1:   for z being Element of X holds (z\x)`=x\z;
      let z be Element of X;
      (z\x)`=x\z by A1;
      hence z`\x`=x\z by Th9;
    end;
    thus (for z being Element of X holds z`\x`=x\z) implies
    (for z being Element of X holds (z\x)`=x\z)
    proof
      assume
A2:   for z being Element of X holds z`\x`=x\z;
      let z be Element of X;
      z`\x`=x\z by A2;
      hence (z\x)`=x\z by Th9;
    end;
  end;
  hence thesis by Th28;
end;

theorem Th31:
  for x being Element of X holds x in AtomSet(X) iff
  for z being Element of X holds ((x\z)`)`=x\z
proof
  let x be Element of X;
  thus x in AtomSet(X) implies for z being Element of X holds ((x\z)`)`=x\z
  proof
    assume
A1: x in AtomSet(X);
    let z be Element of X;
    consider x1 being Element of X such that
A2: x=x1&x1 is atom by A1;
    (z\(z\x))\x=0.X by Th1;
    then (z\(z\x))=x by A2,Def14;
    then ((x\z)`)`=(((z\z)\(z\x))`)` by Th7;
    then ((x\z)`)`=(((z\x)`)`)` by Def5;
    then ((x\z)`)`=(z\x)` by Th8;
    hence thesis by A1,Th30;
  end;
  assume for z being Element of X holds (x\z)``=x\z;
  then ((x\0.X)`)`=x\0.X;
  then (x`)`=x\0.X by Th2;
  then (x`)`=x by Th2;
  hence thesis by Th29;
end;

theorem
  for x being Element of X holds x in AtomSet(X) iff
  for z,u being Element of X holds z\(z\(x\u))=x\u
proof
  let x be Element of X;
  thus x in AtomSet(X) implies
  for z,u being Element of X holds z\(z\(x\u))=x\u
  proof
    assume
A1: x in AtomSet(X);
    let z,u be Element of X;
    x\u =((x\u)`)` by A1,Th31
      .= ((z\z)\(x\u))` by Def5
      .= ((z\(x\u))\z)` by Th7
      .= (z\(x\u))`\z` by Th9;
    then
A2: (x\u)\( z\(z\(x\u)))=0.X by Th1;
    ( z\(z\(x\u)))\(x\u)=0.X by Th1;
    hence thesis by A2,Def7;
  end;
  assume for z,u being Element of X holds z\(z\(x\u))=x\u;
  then (x\u)``=x\u;
  hence thesis by Th31;
end;

theorem Th33:    ::tuilun1.3.3
  for a being Element of AtomSet(X),x being Element of X holds
  a\x in AtomSet(X)
proof
  let a be Element of AtomSet(X),x be Element of X;
  ((a\x)`)`=a\x by Th31;
  hence thesis by Th29;
end;

definition
  let X be BCI-algebra,a,b be Element of AtomSet(X);
  redefine func a\b -> Element of AtomSet(X);
  coherence by Th33;
end;

theorem Th34:
  for x being Element of X holds x` in AtomSet(X)
proof
  let x be Element of X;
  0.X in AtomSet(X) by Th23;
  hence thesis by Th33;
end;

theorem Th35:
  for x being Element of X holds ex a being Element of AtomSet(X) st a<=x
proof
  let x be Element of X;
  take a=x``;
  a\x=0.X by Th1;
  hence thesis by Def11,Th34;
end;

definition
  let X be BCI-algebra;
  attr X is generated_by_atom means
  :Def16:
  for x being Element of X holds
  ex a being Element of AtomSet(X) st a<=x;
end;

definition
  let X be BCI-algebra,a be Element of AtomSet(X);
  func BranchV(a) -> non empty Subset of X equals
  {x where x is Element of X:a<=x};
  coherence
  proof
    set Y={x where x is Element of X:a<=x};
A1: a in Y
    proof
      a\a=0.X by Def5;
      then a <= a by Def11;
      hence thesis;
    end;
    now
      let y be set;
      assume y in Y;
      then consider x being Element of X such that
A2:   y=x & a<=x;
      thus y in the carrier of X by A2;
    end;
    hence thesis by A1,TARSKI:def 3;
  end;
end;

theorem
  for X being BCI-algebra holds X is generated_by_atom
proof
  let X be BCI-algebra;
  for x being Element of X holds (ex a being Element of AtomSet(X)
  st a<=x) by Th35;
  hence thesis by Def16;
end;

theorem
  for a,b being Element of AtomSet(X),x being Element of BranchV(b)
  holds a\x =a\b
proof
  let a,b be Element of AtomSet(X),x be Element of BranchV(b);
  a\b in {x1 where x1 is Element of X:x1 is atom};
  then consider x1 being Element of X such that
A1: a\b=x1 & x1 is atom;
  x in {yy where yy is Element of X:b<=yy};
  then consider yy being Element of X such that
A2: x=yy & b<= yy;
  (a\x)\(a\b)=(a\(a\b))\x by Th7;
  then (a\x)\(a\b)=b\x by Th24;
  then (a\x)\(a\b)=0.X by A2,Def11;
  hence thesis by A1,Def14;
end;

theorem Th38:
  for a being Element of AtomSet(X),x being Element of BCK-part(X)
  holds a\x =a
proof
  let a be Element of AtomSet(X),x be Element of BCK-part(X);
  a\0.X in {x1 where x1 is Element of X:x1 is atom} by Th33;
  then consider x1 being Element of X such that
A1: a\0.X=x1 & x1 is atom;
  x in {x2 where x2 is Element of X:0.X<=x2};
  then consider x2 being Element of X such that
A2: x=x2 & 0.X<=x2;
  (a\x)\(a\0.X)=(a\(a\0.X))\x by Th7;
  then (a\x)\(a\0.X)=(a\a)\x by Th2;
  then (a\x)\(a\0.X)=x` by Def5;
  then (a\x)\(a\0.X)=0.X by A2,Def11;
  then a\x=a\0.X by A1,Def14;
  hence thesis by Th2;
end;

Lm2: for a being Element of AtomSet(X),x being Element of BranchV(a)
holds a\x=0.X
proof
  let a be Element of AtomSet(X),x be Element of BranchV(a);
  x in {x1 where x1 is Element of X:a<=x1};
  then consider x1 being Element of X such that
A1: x=x1 & a<=x1;
  thus a\x =0.X by A1,Def11;
end;

theorem Th39:
  for a,b being Element of AtomSet(X),x being Element of BranchV(a),
  y being Element of BranchV(b) holds x\y in BranchV(a\b)
proof
  let a,b be Element of AtomSet(X),x be Element of BranchV(a),
  y be Element of BranchV(b);
  (a\b)\(x\y)=(((a\b)`)`)\(x\y) by Th29;
  then (a\b)\(x\y)=(x\y)`\(a\b)` by Th7;
  then (a\b)\(x\y)=x`\y`\(a\b)` by Th9;
  then (a\b)\(x\y)=((x`)\((a\b)`))\y` by Th7;
  then (a\b)\(x\y)=((((a\b)`)`)\x)\(y`) by Th7;
  then (a\b)\(x\y)=((a\b)\x)\(y`) by Th29;
  then (a\b)\(x\y)=((a\x)\b)\(y`) by Th7;
  then (a\b)\(x\y)=b`\y` by Lm2;
  then (a\b)\(x\y)=(b\y)` by Th9;
  then (a\b)\(x\y)=(0.X)` by Lm2;
  then (a\b)\(x\y)=0.X by Def5;
  then a\b <= x\y by Def11;
  hence thesis;
end;

theorem
  for a being Element of AtomSet(X),x,y being Element of BranchV(a)
  holds x\y in BCK-part(X)
proof
  let a be Element of AtomSet(X),x,y be Element of BranchV(a);
  set b=a\a;
A1: b=0.X by Def5;
  x\y in BranchV(b) by Th39;
  hence thesis by A1;
end;

theorem
  for a,b being Element of AtomSet(X),x being Element of BranchV(a),
  y being Element of BranchV(b) st a<>b holds not(x\y in BCK-part(X))
proof
  let a,b be Element of AtomSet(X),x be Element of BranchV(a),
  y be Element of BranchV(b);
  assume
A1: a<>b;
  assume
A2: x\y in BCK-part(X);
  x\y in BranchV(a\b) by Th39;
  then consider xy being Element of X such that
A3: x\y=xy & a\b <= xy;
  (a\b)\(x\y) =0.X by A3,Def11;
  then (a\(x\y))\b =0.X by Th7;
  then (a\(x\y))\((a\(x\y))\b) =a\(x\y) by Th2;
  then b = a\(x\y) by Th24;
  hence contradiction by A1,A2,Th38;
end;

theorem
  for a,b being Element of AtomSet(X) st a<>b holds
  BranchV(a) /\ BranchV(b) = {}
proof
  let a,b be Element of AtomSet(X);
  assume
A1: a<>b;
  b in {xx where xx is Element of X:xx is atom};
  then consider xx being Element of X such that
A2: b=xx & xx is atom;
  assume BranchV(a) /\ BranchV(b) <> {};
  then consider c being set such that
A3: c in BranchV(a) /\ BranchV(b) by XBOOLE_0:def 1;
  reconsider z1 = c as Element of BranchV(a) by A3,XBOOLE_0:def 3;
  reconsider z2 = c as Element of BranchV(b) by A3,XBOOLE_0:def 3;
  z1 \ z2 in BranchV(a\b) by Th39;
  then 0.X in {x3 where x3 is Element of X:a\b<=x3}by Def5;
  then consider x3 being Element of X such that
A4: 0.X = x3 & a\b <= x3;
  (a\b)\0.X = 0.X by A4,Def11;
  then a\b = 0.X by Th2;
  hence contradiction by A1,A2,Def14;
end;

::Ideal

definition
  let X be BCI-algebra;
  mode Ideal of X -> non empty Subset of X means
    :Def18:
    0.X in it &
    (for x,y being Element of X st x\y in it & y in it holds x in it);
  existence
  proof
    take X1={0.X};
A1: X1 is Subset of X
    proof
      now
        let xx be set;
        assume xx in X1;
        then xx=0.X by TARSKI:def 1;
        hence xx in the carrier of X;
      end;
      hence thesis by TARSKI:def 3;
    end;
    for x,y being Element of X st x\y in X1 & y in X1 holds x in X1
    proof
      let x,y be Element of X;
      assume x\y in X1 & y in X1;
      then x\y = 0.X & y = 0.X by TARSKI:def 1;
      then x=0.X by Th2;
      hence thesis by TARSKI:def 1;
    end;
    hence thesis by A1,TARSKI:def 1;
  end;
end;

definition
  let X be BCI-algebra, IT be Ideal of X;
  attr IT is closed means
  :Def19:
  for x being Element of IT holds x` in IT;
end;

Lm3: {0.X} is Ideal of X
proof
  set X1={0.X};
A1: X1 is Subset of X
  proof
    now
      let xx be set;
      assume xx in X1;
      then xx=0.X by TARSKI:def 1;
      hence xx in the carrier of X;
    end;
    hence thesis by TARSKI:def 3;
  end;
A2: 0.X in {0.X} by TARSKI:def 1;
  for x,y being Element of X st x\y in {0.X} & y in {0.X} holds x in {0.X}
  proof
    let x,y be Element of X;
    set X1={0.X};
    assume x\y in X1 & y in X1;
    then x\y = 0.X & y = 0.X by TARSKI:def 1;
    then x=0.X by Th2;
    hence thesis by TARSKI:def 1;
  end;
  hence thesis by A1,A2,Def18;
end;

Lm4: for X1 being Ideal of X st X1={0.X} holds
for x being Element of X1 holds x` in { 0.X }
proof
  let X1 be Ideal of X;
  assume
A1: X1={0.X};
  let x be Element of X1;
  x=0.X by A1,TARSKI:def 1;
  then x`=0.X by Def5;
  hence x` in {0.X} by TARSKI:def 1;
end;

registration
  let X;
  cluster closed Ideal of X;
  existence
  proof
    set X1={0.X};
    reconsider X1 as Ideal of X by Lm3;
    take X1;
    for x being Element of X1 holds x` in X1 by Lm4;
    hence thesis by Def19;
  end;
end;

theorem
  {0.X} is closed Ideal of X
proof
  set X1={0.X};
  reconsider X1 as Ideal of X by Lm3;
  for x being Element of X1 holds x` in X1 by Lm4;
  hence thesis by Def19;
end;

theorem
  the carrier of X is closed Ideal of X
proof
A1: the carrier of X is non empty Subset of X by ZFMISC_1:def 1;
A2: 0.X in the carrier of X &
  for x being Element of X holds x` in the carrier of X;
  for x,y being Element of the carrier of X st x\y in the carrier of X
  & y in the carrier of X holds x in the carrier of X;
  hence thesis by A1,A2,Def18,Def19;
end;

theorem
  BCK-part(X) is closed Ideal of X
proof
  set X1=BCK-part(X);
A1: 0.X in BCK-part(X) by Th19;
  for x,y being Element of X st x\y in X1 & y in X1 holds x in X1
  proof
    let x,y be Element of X such that
A2: x\y in X1 & y in X1;
    consider x1 being Element of X such that
A3: x\y=x1 & 0.X<= x1 by A2;
    consider x2 being Element of X such that
A4: y=x2 & 0.X<= x2 by A2;
    (x\y)`=0.X by A3,Def11;
    then x`\y`=0.X by Th9;
    then x`\0.X = 0.X by A4,Def11;
    then x`=0.X by Th2;
    then 0.X<= x by Def11;
    hence x in X1;
  end;
  then reconsider X1 as Ideal of X by A1,Def18;
  now
    let x be Element of X1;
    x in X1;
    then consider x1 being Element of X such that
A5: x=x1 & 0.X<= x1;
    (x`)=0.X by A5,Def11;
    then (x`)`=0.X by Def5;
    then 0.X <=x` by Def11;
    hence x` in X1;
  end;
  hence thesis by Def19;
end;

Lm5: IT is Ideal of X implies (for x,y being Element of IT holds
{z where z is Element of X : z\x<=y} c= IT)
proof
  assume
A1: IT is Ideal of X;
  then
A2: 0.X in IT by Def18;
  let x,y be Element of IT;
  for ss being set st ss in {z where z is Element of X : z\x<=y}
  holds ss in IT
  proof
    let ss be set;
    assume ss in {z where z is Element of X : z\x<=y};
    then consider z being Element of X such that
A3: ss=z & z\x <= y;
    reconsider ss as Element of X by A3;
    (ss\x)\y in IT by A2,A3,Def11;
    then ss\x in IT by A1,Def18;
    hence thesis by A1,Def18;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  IT is Ideal of X implies (for x,y being Element of X st
  x in IT & y<=x holds y in IT)
proof
  assume
A1: IT is Ideal of X;
  then
A2: 0.X is Element of IT by Def18;
  let x,y be Element of X;
  assume
A3: x in IT & y<=x;
  then y\0.X <= x by Th2;
  then
A4: y in {z where z is Element of X : z\0.X<=x};
  {z where z is Element of X : z\0.X<=x} c= IT by A1,A2,A3,Lm5;
  hence y in IT by A4;
end;

begin :: Several Classes of BCI-algebra---associative BCI-algebra

definition
  let IT be BCI-algebra;
  attr IT is associative means
  :Def20:
  for x,y,z being Element of IT holds x\y\z = x\(y\z);
  attr IT is quasi-associative means
  :Def21:
  for x being Element of IT holds x``=x`;
  attr IT is positive-implicative means
  :Def22:
  for x,y being Element of IT holds (x\(x\y))\(y\x)=x\(x\(y\(y\x)));
  attr IT is weakly-positive-implicative means
  :Def23:
  for x,y,z being Element of IT holds (x\y)\z=((x\z)\z)\(y\z);
  attr IT is implicative means
  :Def24:
  for x,y being Element of IT holds (x\(x\y))\(y\x)=y\(y\x);
  attr IT is weakly-implicative means
  for x,y being Element of IT holds (x\(y\x))\(y\x)`=x;
  attr IT is p-Semisimple means
  :Def26:
  for x,y being Element of IT holds x\(x\y) = y;
  attr IT is alternative means
  :Def27:
  for x,y being Element of IT holds
  x\(x\y) = (x\x)\y & (x\y)\y=x\(y\y);
end;

registration
  cluster BCI-EXAMPLE -> implicative positive-implicative p-Semisimple
    associative weakly-implicative weakly-positive-implicative;
  coherence
  proof
    set IT = BCI-EXAMPLE;
A1: IT is implicative
    proof
      let x,y be Element of IT;
      thus (x\(x\y))\(y\x)=y\(y\x) by STRUCT_0:def 10;
    end;
A2: IT is positive-implicative
    proof
      let x,y be Element of IT;
      thus (x\(x\y))\(y\x)=x\(x\(y\(y\x))) by STRUCT_0:def 10;
    end;
A3: IT is p-Semisimple
    proof
      let x,y be Element of IT;
      x\(x\y)={}&{}= y by CARD_1:87,TARSKI:def 1;
      hence thesis;
    end;
A4: IT is associative
    proof
      let x,y,z be Element of IT;
      (x\y)\z={}&x\(y\z)={} by CARD_1:87,TARSKI:def 1;
      hence (x\y)\z=x\(y\z);
    end;
A5: IT is weakly-implicative
    proof
      let x,y be Element of IT;
      (x\(y\x))\(y\x)`={}&x={} by CARD_1:87,TARSKI:def 1;
      hence (x\(y\x))\(y\x)`=x;
    end;
    IT is weakly-positive-implicative
    proof
      let x,y,z be Element of IT;
      thus (x\y)\z=((x\z)\z)\(y\z) by STRUCT_0:def 10;
    end;
    hence thesis by A1,A2,A3,A4,A5;
  end;
end;

registration
  cluster implicative positive-implicative p-Semisimple
    associative weakly-implicative weakly-positive-implicative BCI-algebra;
  existence
  proof
    take BCI-EXAMPLE;
    thus thesis;
  end;
end;

Lm6: (for x,y being Element of X holds y\x=x\y) implies X is associative
proof
  assume
A1: for x,y being Element of X holds y\x=x\y;
  let x,y,z be Element of X;
  x\(y\z) = (y\z)\x by A1
    .=(y\x)\z by Th7;
  hence thesis by A1;
end;

Lm7: (for x holds x`=x) implies (for x,y holds x\y=y\x)
proof
  assume
A1: for x holds x`=x;
  let x,y;
A2: (x\y)\(y\x)=(x`\y)\(y\x) by A1
    .=(x`\y`)\(y\x) by A1
    .=0.X by Th1;
  (y\x)\(x\y)=(y`\x)\(x\y) by A1
    .=(y`\x`)\(x\y) by A1
    .=0.X by Th1;
  hence thesis by A2,Def7;
end;

theorem Th47:
  X is associative iff (for x being Element of X holds x`=x)
proof
  thus X is associative implies(for x being Element of X holds x`=x)
  proof
    assume
A1: X is associative;
    let x be Element of X;
A2: x`\x=(x\x)` by A1,Def20
      .=(0.X)` by Def5
      .=0.X by Def5;
    x\x`=(x\0.X)\x by A1,Def20
      .=x\x by Th2
      .=0.X by Def5;
    hence thesis by A2,Def7;
  end;
  assume for x being Element of X holds x`=x;
  then for x,y holds x\y=y\x by Lm7;
  hence thesis by Lm6;
end;

theorem Th48:
  (for x,y being Element of X holds y\x=x\y) iff X is associative
proof thus
  (for x,y being Element of X holds y\x=x\y) implies X is associative by Lm6;
  assume X is associative;
  then for x being Element of X holds x`=x by Th47;
  hence thesis by Lm7;
end;

theorem Th49:
  for X being non empty BCIStr_0 holds (X is associative BCI-algebra
  iff (for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x))
proof
  let X be non empty BCIStr_0;
  thus X is associative BCI-algebra implies
  (for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x)
  proof
    assume
A1: X is associative BCI-algebra;
    let x,y,z be Element of X;
    (z\y)\((y\x)\(z\x))=((z\y)\(y\x))\(z\x) by A1,Def20;
    then (z\y)\((y\x)\(z\x)) = ((z\y)\(z\x))\(y\x) by A1,Th7;
    then (z\y)\((y\x)\(z\x)) = ((z\y)\(z\x))\(x\y) by A1,Th48;
    then
A2: (z\y)\((y\x)\(z\x)) = 0.X by A1,Th1;
    ((y\x)\(z\x))\(z\y)=((y\x)\(z\x))\(y\z) by A1,Th48;
    then ((y\x)\(z\x))\(z\y)=0.X by A1,Def3;
    hence thesis by A1,A2,Def7,Th2;
  end;
  thus (for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x)
  implies X is associative BCI-algebra
  proof
    assume
A3: for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x;
A4: for x,y being Element of X holds y\x=x\y
    proof
      let x,y be Element of X;
      (y\0.X)\(x\0.X)=x\y by A3;
      then y\(x\0.X)=x\y by A3;
      hence thesis by A3;
    end;
    (X is_I & X is_BCI-4 &for x,y,z being Element of X holds
    ((x\y)\(x\z))\(z\y)=0.X & (x\(x\y))\y = 0.X )
    proof
A5:   for a being Element of X holds a\a=0.X
      proof
        let a be Element of X;
        a`\a`=(0.X)` by A3;
        then (a\0.X)\a`=(0.X)` by A4;
        then (a\0.X)\(a\0.X)=(0.X)` by A4;
        then a\a=(0.X)` by A3;
        hence a\a=0.X by A3;
      end;
      hence X is_I by Def5;
      thus X is_BCI-4
      proof
        for x,y being Element of X holds (x\y=0.X&y\x=0.X implies x = y)
        proof
          let x,y be Element of X;
          assume
A6:       x\y = 0.X & y\x = 0.X;
          x`\(y\x)=y\0.X by A3;
          then (x\0.X)\(y\x)=y\0.X by A4;
          then (x\0.X)\(x\y)=y\0.X by A4;
          then x\(x\y)=y\0.X by A3;
          then y=x\(x\y) by A3
            .=x by A3,A6;
          hence thesis;
        end;
        hence thesis by Def7;
      end;
      thus for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X &
      (x\(x\y))\y = 0.X
      proof
        let x,y,z be Element of X;
        thus ((x\y)\(x\z))\(z\y)=0.X
        proof
          ((x\y)\(x\z))\(z\y)=((y\x)\(x\z))\(z\y) by A4
            .=((y\x)\(z\x))\(z\y) by A4
            .=(z\y)\(z\y) by A3;
          hence thesis by A5;
        end;
        thus (x\(x\y))\y = 0.X
        proof
          x`\(y\x)=y\0.X by A3;
          then (x\0.X)\(y\x)=y\0.X by A4;
          then (x\0.X)\(x\y)=y\0.X by A4;
          then x\(x\y)=y\0.X by A3;
          then (x\(x\y))\y=y\y by A3;
          hence thesis by A5;
        end;
      end;
    end;
    then reconsider Y=X as BCI-algebra by Th1;
    Y is associative by A4,Th48;
    hence thesis;
  end;
end;

theorem Th50:
  for X being non empty BCIStr_0 holds (X is associative BCI-algebra
  iff (for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x))
proof
  let X be non empty BCIStr_0;
  thus X is associative BCI-algebra implies
  (for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x)
  proof
    assume
A1: X is associative BCI-algebra;
    let x,y,z be Element of X;
    (y\x)\(z\x)=z\y & x\0.X=x by A1,Th49;
    then (x\y)\(z\x)=z\y & x\0.X=x by A1,Th48;
    hence thesis by A1,Th48;
  end;
  assume
A2: for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x;
  for x,y,z being Element of X holds (y\x)\(z\x)=z\y & x\0.X=x
  proof
    let x,y,z be Element of X;
A3: for x,y being Element of X holds y\x=x\y
    proof
      let x,y be Element of X;
      y`\x`=x\y by A2;
      then y\x`=x\y by A2;
      hence thesis by A2;
    end;
    (x\y)\(x\z)=z\y & x`=x by A2;
    then (y\x)\(x\z)=z\y & x\0.X=x by A3;
    hence thesis by A3;
  end;
  hence thesis by Th49;
end;

theorem
  for X being non empty BCIStr_0 holds (X is associative BCI-algebra
  iff (for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x))
proof
  let X be non empty BCIStr_0;
  thus X is associative BCI-algebra implies
  (for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x)
  proof
    assume
A1: X is associative BCI-algebra;
    let x,y,z be Element of X;
    (y\x)\(z\x)=z\y & x\0.X=x by A1,Th49;
    then (x\y)\(z\x)=z\y & x\0.X=x by A1,Th48;
    then (x\y)\(x\z)=z\y & x\0.X=x by A1,Th48;
    hence thesis by A1,Th48;
  end;
  assume
A2: for x,y,z being Element of X holds (x\y)\(x\z)=y\z & x\0.X=x;
  for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x`=x
  proof
    let x,y,z be Element of X;
A3: for x,y being Element of X holds y\x=x\y
    proof
      let x,y be Element of X;
      (x\0.X)\(x\0.X)=(0.X)` by A2;
      then x\(x\0.X)=(0.X)` by A2;
      then x\x=(0.X)` by A2;
      then
A4:   x\x=0.X by A2;
      (x\y)\(x\x)=y\x by A2;
      hence thesis by A2,A4;
    end;
    (x\y)\(x\z)=y\z & x\0.X=x by A2;
    hence thesis by A3;
  end;
  hence thesis by Th50;
end;

begin :: Several Classes of BCI-algebra----p-Semisimple BCI-algebra

theorem
  X is p-Semisimple iff for x being Element of X holds x is atom
proof
  thus X is p-Semisimple implies for x being Element of X holds x is atom
  proof
    assume
A1: X is p-Semisimple;
    let x be Element of X;
    now
      let z be Element of X;
      assume z\x=0.X;
      then z\0.X = x by A1,Def26;
      hence z=x by Th2;
    end;
    hence thesis by Def14;
  end;
  assume
A2: for x being Element of X holds x is atom;
  for x,y being Element of X holds x\(x\y) = y
  proof
    let x,y be Element of X;
A3: y is atom by A2;
    (x\(x\y))\y=0.X by Th1;
    hence thesis by A3,Def14;
  end;
  hence thesis by Def26;
end;

theorem
  X is p-Semisimple implies BCK-part(X)={0.X}
proof
  assume
A1: X is p-Semisimple;
  thus BCK-part(X) c= {0.X}
  proof
    let x be set;
    assume x in BCK-part(X);
    then consider x1 being Element of X such that
A2: x=x1 & 0.X<=x1;
    reconsider x as Element of X by A2;
    (x`)`=x by A1,Def26;
    then (0.X)`=x by A2,Def11;
    then x=0.X by Def5;
    hence thesis by TARSKI:def 1;
  end;
  thus {0.X} c= BCK-part(X)
  proof
    let x be set;
    assume
A3: x in {0.X};
    then reconsider x as Element of X by TARSKI:def 1;
    x=0.X by A3,TARSKI:def 1;
    then x`=0.X by Def5;
    then 0.X <= x by Def11;
    hence thesis;
  end;
end;

Lm8: (for x holds x``=x) iff for x,y holds y\(y\x) = x
proof
  thus (for x holds x``=x) implies for x,y holds y\(y\x) = x
  proof
    assume
A1: for x holds x``=x;
    let x,y;
A2: x\(y\(y\x))= (x\(y\(y\x)))`` by A1
      .=(x`\(y\(y\x))`)` by Th9
      .=0.X \((x`\(y\(y\x))`)\0.X) by Th2
      .=0.X \(((0.X \x)\((y\(y\x))`))\((y\(y\x))\x)) by Th1
      .=0.X \0.X by Th1
      .=0.X by Def5;
    (y\(y\x))\x=0.X by Th1;
    hence thesis by A2,Def7;
  end;
  thus thesis;
end;

Lm9: (for x,y holds y\(y\x) = x) iff for x,y,z holds (z\y)\(z\x) = x\y
proof
  thus (for x,y holds y\(y\x) = x) implies for x,y,z holds (z\y)\(z\x) = x\y
  proof
    assume
A1: for x,y holds y\(y\x) = x;
    let x,y,z;
    (z\y)\(z\x)= (z\(z\x))\y by Th7;
    hence thesis by A1;
  end;
  assume
A2: for x,y,z holds (z\y)\(z\x) = x\y;
  let x,y;
  (y\0.X)\(y\x) = x\0.X by A2;
  then y\(y\x) = x\0.X by Th2;
  hence thesis by Th2;
end;

theorem Th54:
  X is p-Semisimple iff (for x being Element of X holds x`` = x)
proof
  (for x being Element of X holds x`` = x) implies X is p-Semisimple
  proof
    assume
A1: for x being Element of X holds x`` = x;
    now
      let x,y be Element of X;
A2:   y\(x\(x\y))=(y\(x\(x\y)))`` by A1
        .=(y`\(x\(x\y))`)` by Th9
        .=0.X \(((0.X \y)\((x\(x\y))`))\0.X) by Th2
        .=0.X \(((0.X \y)\((x\(x\y))`))\((x\(x\y))\y)) by Th1
        .=0.X \0.X by Th1
        .=0.X by Def5;
      (x\(x\y))\y=0.X by Th1;
      hence x\(x\y) = y by A2,Def7;
    end;
    hence thesis by Def26;
  end;
  hence thesis by Def26;
end;

theorem Th55:
  X is p-Semisimple iff (for x,y holds y\(y\x) = x)
proof
  X is p-Semisimple iff (for x being Element of X holds x`` = x) by Th54;
  hence thesis by Lm8;
end;

theorem Th56:
  X is p-Semisimple iff (for x,y,z holds (z\y)\(z\x) = x\y)
proof
  X is p-Semisimple iff (for x,y holds y\(y\x) = x)by Th55;
  hence thesis by Lm9;
end;

theorem Th57:
  X is p-Semisimple iff (for x,y,z holds x\(z\y) = y\(z\x))
proof
  thus X is p-Semisimple implies (for x,y,z holds x\(z\y) = y\(z\x))
  proof
    assume
A1: X is p-Semisimple;
    let x,y,z;
    x\(z\y) =(z\(z\x))\(z\y)by A1,Def26;
    then
A2: (x\(z\y))\(y\(z\x))=0.X by Th1;
    y\(z\x) =(z\(z\y))\(z\x) by A1,Def26;
    then (y\(z\x))\(x\(z\y))=0.X by Th1;
    hence thesis by A2,Def7;
  end;
  assume
A3: for x,y,z holds x\(z\y) = y\(z\x);
  for x holds x`` = x
  proof
    let x;
    x`` = x\(0.X)` by A3
      .=x\0.X by Def5;
    hence thesis by Th2;
  end;
  hence thesis by Th54;
end;

Lm10: X is p-Semisimple implies (for x,y,z,u holds
(x\u)\(z\y)=(y\u)\(z\x)&(x\u)\(z\y)=(x\z)\(u\y))
proof
  assume
A1: X is p-Semisimple;
  let x,y,z,u;
A2: (x\u)\(z\y)=y\(z\(x\u)) by A1,Th57
    .=y\(u\(x\z)) by A1,Th57
    .=(x\z)\(u\y) by A1,Th57;
  (x\u)\(z\y)=(x\(z\y))\u by Th7
    .=(y\(z\x))\u by A1,Th57;
  hence thesis by A2,Th7;
end;

Lm11: X is p-Semisimple implies (for x,y holds y`\(0.X \x)=x\y)
proof
  assume
A1: X is p-Semisimple;
  let x,y;
  y`\(0.X \x)=(x\y)\(0.X \0.X) by A1,Lm10
    .=(x\y)\0.X by Def5;
  hence thesis by Th2;
end;

Lm12: X is p-Semisimple implies (for x,y,z holds (x\y)\(z\y)=x\z)
proof
  assume
A1: X is p-Semisimple;
  let x,y,z;
  (x\y)\(z\y)=(x\z)\(y\y) by A1,Lm10
    .=(x\z)\0.X by Def5;
  hence thesis by Th2;
end;

Lm13: X is p-Semisimple implies (for x,y,z st x\y=x\z holds y=z)
proof
  assume
A1: X is p-Semisimple;
  let x,y,z;
  assume
A2: x\y=x\z;
  (x\y)\(x\z)=(z\y)\(x\x) by A1,Lm10;
  then (x\y)\(x\z)=(z\y)\0.X by Def5;
  then (x\y)\(x\z)=z\y by Th2;
  then
A3: 0.X=z\y by A2,Def5;
  (x\z)\(x\y)=(y\z)\(x\x) by A1,Lm10;
  then (x\z)\(x\y)=(y\z)\0.X by Def5;
  then (x\z)\(x\y)=y\z by Th2;
  then 0.X=y\z by A2,Def5;
  hence thesis by A3,Def7;
end;

Lm14: X is p-Semisimple implies for x,y,z holds x\(y\z)=(z\y)\x`
proof
  assume
A1: X is p-Semisimple;
  let x,y,z;
  x\(y\z)=z\(y\x) by A1,Th57
    .=(z\0.X)\(y\x) by Th2;
  hence thesis by A1,Lm10;
end;

Lm15: X is p-Semisimple implies for x,y,z st y\x=z\x holds y=z
proof
  assume
A1: X is p-Semisimple;
  let x,y,z;
  assume
A2: y\x=z\x;
A3: y\z=(y\x)\(z\x) by A1,Lm12
    .=0.X by A2,Def5;
  z\y=(z\x)\(y\x) by A1,Lm12
    .=0.X by A2,Def5;
  hence thesis by A3,Def7;
end;

theorem
  X is p-Semisimple iff (for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x))
proof
  thus X is p-Semisimple implies
  (for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x))by Lm10;
  thus (for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x)) implies X is p-Semisimple
  proof
    assume
A1: for x,y,z,u holds (x\u)\(z\y) = (y\u)\(z\x);
    for x,y,z holds x\(z\y) = y\(z\x)
    proof
      let x,y,z;
      (x\0.X)\(z\y) = (y\0.X)\(z\x) by A1;
      then x\(z\y)= (y\0.X)\(z\x) by Th2;
      hence thesis by Th2;
    end;
    hence thesis by Th57;
  end;
end;

theorem Th59:
  X is p-Semisimple iff (for x,z holds z`\x` = x\z)
proof
  thus X is p-Semisimple implies (for x,z holds z`\x` = x\z) by Lm11;
  assume
A1: for x,z holds z`\x` = x\z;
  for x holds x`` = x
  proof
    let x;
    (0.X)`\x` = x\0.X by A1;
    then (x`)` = x\0.X by Th2;
    hence thesis by Th2;
  end;
  hence thesis by Th54;
end;

theorem
  X is p-Semisimple iff (for x,z holds (x\z)`` = x\z)
proof
  thus X is p-Semisimple implies (for x,z holds (x\z)`` = x\z)
  proof
    assume
A1: X is p-Semisimple;
    let x,z;
    (x\z)``=(x`\z`)` by Th9
      .=(z\x)` by A1,Th59
      .=z`\x` by Th9;
    hence thesis by A1,Th59;
  end;
  assume
A2: for x,z holds (x\z)`` = x\z;
  now
    let x;
    (x\0.X)``=x\0.X by A2;
    then (x`)`=x\0.X by Th2;
    hence x``=x by Th2;
  end;
  hence thesis by Th54;
end;

theorem
  X is p-Semisimple iff (for x,u,z holds z\(z\(x\u)) = x\u)
proof
  thus X is p-Semisimple implies (for x,u,z holds z\(z\(x\u)) = x\u)
  proof
    assume
A1: X is p-Semisimple;
    let x,u,z;
    (z\(z\(x\u)))\(x\u)=0.X by Th1
      .= (x\u)\(x\u) by Def5;
    hence thesis by A1,Lm15;
  end;
  assume
A2: for x,u,z holds z\(z\(x\u)) = x\u;
  now
    let x;
    ((x\0.X)`)` = x\0.X by A2;
    then ((x\0.X)`)` = x by Th2;
    hence x`` = x by Th2;
  end;
  hence thesis by Th54;
end;

theorem Th62:  ::TL2232:
  X is p-Semisimple iff (for x st x`=0.X holds x=0.X)
proof
  thus X is p-Semisimple implies(for x st x`=0.X holds x=0.X)
  proof
    assume
A1: X is p-Semisimple;
    let x;
    assume x`=0.X;
    then (x`)`=0.X by Def5;
    hence thesis by A1,Def26;
  end;
  assume
A2: for x st x`=0.X holds x=0.X;
  for x holds x`` = x
  proof
    let x;
    (x\x``)`=x`\x``` by Th9
      .=x`\x` by Th8
      .=0.X by Def5;
    then
A3: x\((x)`)`=0.X by A2;
    ((x)`)`\x=0.X by Th1;
    hence thesis by A3,Def7;
  end;
  hence thesis by Th54;
end;

theorem Th63:
  X is p-Semisimple iff (for x,y holds x\y`=y\x`)
proof
  thus X is p-Semisimple implies (for x,y holds x\y`=y\x`) by Th57;
  assume
A1: for x,y holds x\y`=y\x`;
  now
    let x;
    x\(0.X)`=(x`)` by A1;
    then x\0.X=(x`)` by Th2;
    hence x=x`` by Th2;
  end;
  hence thesis by Th54;
end;

theorem
  X is p-Semisimple iff (for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u))
proof
  thus X is p-Semisimple implies
  (for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u))by Lm10;
  assume
A1: for x,y,z,u holds (x\y)\(z\u)=(x\z)\(y\u);
  for x,z holds z`\x` = x\z
  proof
    let x,z;
    (z\x)`=(x\x)\(z\x) by Def5;
    then (z\x)`=(x\z)\(x\x) by A1;
    then (z\x)`=(x\z)\0.X by Def5;
    then (z\x)`=x\z by Th2;
    hence thesis by Th9;
  end;
  hence thesis by Th59;
end;

theorem
  X is p-Semisimple iff (for x,y,z holds (x\y)\(z\y)=x\z)
proof
  thus X is p-Semisimple implies (for x,y,z holds (x\y)\(z\y)=x\z)by Lm12;
  assume
A1: for x,y,z holds (x\y)\(z\y)=x\z;
  for x,z holds z`\x` = x\z
  proof
    let x,z;
    (z\x)`=(x\x)\(z\x)by Def5;
    then (z\x)`=x\z by A1;
    hence thesis by Th9;
  end;
  hence thesis by Th59;
end;

theorem
  X is p-Semisimple iff (for x,y,z holds x\(y\z)=(z\y)\x`)
proof
  thus X is p-Semisimple implies (for x,y,z holds x\(y\z)=(z\y)\x`)by Lm14;
  assume
A1: for x,y,z holds x\(y\z)=(z\y)\x`;
  for x,y holds x\y`=y\x`
  proof
    let x,y;
    x\y`=(y\0.X)\x` by A1;
    hence x\y`=y\x` by Th2;
  end;
  hence thesis by Th63;
end;

theorem
  X is p-Semisimple iff (for x,y,z st y\x=z\x holds y=z)
proof
  thus X is p-Semisimple implies (for x,y,z st y\x=z\x holds y=z)by Lm15;
  assume
A1: for x,y,z st y\x=z\x holds y=z;
  for x,y holds x\(x\y) = y
  proof
    let x,y;
    (x\(x\y))\y = 0.X by Th1;
    then (x\(x\y))\y = y\y by Def5;
    hence thesis by A1;
  end;
  hence thesis by Def26;
end;

theorem
  X is p-Semisimple iff (for x,y,z st x\y=x\z holds y=z)
proof
  thus X is p-Semisimple implies (for x,y,z st x\y=x\z holds y=z)by Lm13;
  assume
A1: for x,y,z st x\y=x\z holds y=z;
  for x st x`=0.X holds x=0.X
  proof
    let x;
    assume x`=0.X;
    then x`=(0.X)` by Def5;
    hence thesis by A1;
  end;
  hence thesis by Th62;
end;

theorem
  for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra iff
  (for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x\0.X=x))
proof
  let X be non empty BCIStr_0;
  thus X is p-Semisimple BCI-algebra implies (for x,y,z being Element of X
  holds (x\y)\(x\z)=z\y & x\0.X=x) by Th2,Th56;
  assume
A1: for x,y,z being Element of X holds (x\y)\(x\z)=z\y & x\0.X=x;
A2: X is_I
  proof
    now
      let x be Element of X;
      x\x=(x\0.X)\x by A1
        .=(x\0.X)\(x\0.X) by A1
        .=(0.X)` by A1;
      hence x\x=0.X by A1;
    end;
    hence thesis by Def5;
  end;
A3: X is_BCI-4
  proof
    now
      let x,y be Element of X;
      assume
A4:   x\y = 0.X & y\x = 0.X;
      x=x\0.X by A1
        .=(x\0.X)\(x\y) by A1,A4
        .= y\0.X by A1;
      hence x=y by A1;
    end;
    hence thesis by Def7;
  end;
  now
    let x,y,z be Element of X;
    thus ((x\y)\(x\z))\(z\y)=0.X
    proof
      ((x\y)\(x\z))\(z\y)=(z\y)\(z\y) by A1
        .=((z\y)\0.X)\(z\y) by A1
        .=((z\y)\0.X)\((z\y)\0.X) by A1
        .=(0.X)` by A1;
      hence thesis by A1;
    end;
    thus (x\(x\y))\y = 0.X
    proof
      (x\(x\y))\y=((x\0.X)\(x\y))\y by A1
        .=(y\0.X)\y by A1
        .=(y\0.X)\(y\0.X) by A1
        .=(0.X)` by A1;
      hence thesis by A1;
    end;
    thus for x,y being Element of X holds x\(x\y) = y
    proof
      let x,y be Element of X;
      x\(x\y)=(x\0.X)\(x\y) by A1;
      then x\(x\y)= y\0.X by A1;
      hence thesis by A1;
    end;
  end;
  hence thesis by A2,A3,Def26,Th1;
end;

theorem
  for X being non empty BCIStr_0 holds (X is p-Semisimple BCI-algebra iff
  (X is_I &for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x))
proof
  let X be non empty BCIStr_0;
  thus X is p-Semisimple BCI-algebra implies
  (X is_I & for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x)
  by Th2,Th57;
  assume
A1: X is_I & for x,y,z being Element of X holds x\(y\z)=z\(y\x) & x\0.X=x;
A2: X is_BCI-4
  proof
    now
      let x,y be Element of X;
      assume
A3:   x\y = 0.X & y\x = 0.X;
      x=x\0.X by A1
        .=y\(x\x) by A1,A3
        .= y\0.X by A1,Def5;
      hence x=y by A1;
    end;
    hence thesis by Def7;
  end;
  now
    let x,y,z be Element of X;
    thus x\x=0.X by A1,Def5;
    thus ((x\y)\(x\z))\(z\y)=0.X
    proof
      ((x\y)\(x\z))\(z\y)=(z\(x\(x\y)))\(z\y) by A1
        .=(z\(y\(x\x)))\(z\y) by A1
        .=(z\(y\0.X))\(z\y) by A1,Def5
        .=(z\y)\(z\y) by A1;
      hence thesis by A1,Def5;
    end;
    thus (x\(x\y))\y = 0.X
    proof
      (x\(x\y))\y=(y\(x\x))\y by A1
        .=(y\0.X)\y by A1,Def5
        .=y\y by A1;
      hence thesis by A1,Def5;
    end;
    thus for x,y being Element of X holds x\(x\y) = y
    proof
      let x,y be Element of X;
      x\(x\y)=y\(x\x) by A1;
      then x\(x\y)= y\0.X by A1,Def5;
      hence thesis by A1;
    end;
  end;
  hence thesis by A1,A2,Def26,Th1;
end;

begin :: Several Classes of BCI-algebra----quasi-associative BCI-algebra

Lm16: (for x being Element of X holds x`<=x) implies
for x,y being Element of X holds (x\y)`=(y\x)`
proof
  assume
A1: for x being Element of X holds x`<=x;
  let x,y be Element of X;
  (x\y)`=(((x\y)`)`)` by Th8
    .=((x`\y`)`)` by Th9
    .=(x``\y``)` by Th9
    .=((((y)`)`)`\x`)` by Th7
    .=(y`\x`)` by Th8
    .=(y\x)`` by Th9;
  then (x\y)`<= (y\x)` by A1;
  then
A2: ((x\y)`)\((y\x)`)=0.X by Def11;
  (y\x)`=(y\x)``` by Th8
    .=(y`\x`)`` by Th9
    .=(y``\x``)` by Th9
    .=((((x`)`)`)\y`)` by Th7
    .=(x`\y`)` by Th8
    .=(x\y)`` by Th9;
  then (y\x)`<= (x\y)` by A1;
  then ((y\x)`)\((x\y)`)=0.X by Def11;
  hence thesis by A2,Def7;
end;

Lm17: (for x,y being Element of X holds (x\y)`=(y\x)`)implies
(for x,y being Element of X holds x`\y=(x\y)`)
proof
  assume
A1: for x,y being Element of X holds (x\y)`=(y\x)`;
  let x,y be Element of X;
  thus (x\y)`=x`\y` by Th9
    .=y``\x by Th7
    .=(y\0.X)`\x by A1
    .=y`\x by Th2
    .=x`\y by Th7;
end;

Lm18: (for x,y being Element of X holds x`\y=(x\y)`) implies
(for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X))
proof
  assume
A1: for x,y being Element of X holds x`\y=(x\y)`;
  let x,y be Element of X;
  ((x\y)\(y\x))`=(x\y)`\(y\x) by A1
    .=(x`\y`)\(y\x) by Th9
    .=(y``\x)\(y\x) by Th7
    .=(y`\x)`\(y\x) by A1
    .=((y\x)``)\(y\x) by A1
    .=0.X by Th1;
  then 0.X <= (x\y)\(y\x) by Def11;
  hence thesis;
end;

Lm19: (for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X))implies
X is quasi-associative
proof
  assume
A1: for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X);
  for x being Element of X holds (x`)`=x`
  proof
    let x be Element of X;
    x`\x=x`\(x\0.X) by Th2;
    then x`\x in {x1 where x1 is Element of X:0.X<=x1} by A1;
    then consider x1 being Element of X such that
A2: x`\x=x1 & 0.X<=x1;
    (x`\x)`=0.X by A2,Def11;
    then
A3: (x`)`\x`=0.X by Th9;
    x\x`=(x\0.X)\x` by Th2;
    then x\x` in {x2 where x2 is Element of X:0.X<=x2}by A1;
    then consider x2 being Element of X such that
A4: x\x`=x2 & 0.X<=x2;
    (x\x`)`=0.X by A4,Def11;
    then x`\(x`)`=0.X by Th9;
    hence thesis by A3,Def7;
  end;
  hence thesis by Def21;
end;

Lm20: (for x being Element of X holds x`<=x) iff
(for x,y,z being Element of X holds (x\y)\z<=x\(y\z))
proof
  thus (for x being Element of X holds x`<=x) implies
  (for x,y,z being Element of X holds (x\y)\z<=x\(y\z))
  proof
    assume
A1: for x being Element of X holds x`<=x;
    let x,y,z be Element of X;
    z`<=z by A1;
    then
A2: z`\z=0.X by Def11;
A3: ((x\y)\z)\(x\(y\z)) = ((x\y)\(x\(y\z)))\z by Th7
      .=((x\(x\(y\z)))\y)\z by Th7;
    (x\(x\(y\z)))\(y\z) =0.X by Th1;
    then ((x\(x\(y\z)))\y)\((y\z)\y) =0.X by Th4;
    then ((x\y)\z)\(x\(y\z))\(((y\z)\y)\z) =0.X by A3,Th4;
    then ((x\y)\z)\(x\(y\z))\(((y\y)\z)\z) =0.X by Th7;
    then ((x\y)\z)\(x\(y\z))\0.X =0.X by A2,Def5;
    then ((x\y)\z)\(x\(y\z)) =0.X by Th2;
    hence thesis by Def11;
  end;
  assume
A4: for x,y,z being Element of X holds (x\y)\z<=x\(y\z);
  let x be Element of X;
  (0.X)`\x <= (x`)` by A4;
  then x`<=(x`)`by Def5;
  then x`\((x`)`)=0.X by Def11;
  then ((x`)`)`\x=0.X by Th7;
  then x`\x=0.X by Th8;
  hence thesis by Def11;
end;

theorem Th71:
  X is quasi-associative iff (for x being Element of X holds x`<=x)
proof
  thus X is quasi-associative implies (for x being Element of X holds x`<=x)
  proof
    assume
A1: X is quasi-associative;
    let x be Element of X;
    (x`)`\x=0.X by Th1;
    then x`\x=0.X by A1,Def21;
    hence thesis by Def11;
  end;
  assume for x being Element of X holds x`<=x;
  then for x,y being Element of X holds (x\y)`=(y\x)` by Lm16;
  then for x,y being Element of X holds x`\y=(x\y)` by Lm17;
  then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm18;
  hence thesis by Lm19;
end;

theorem Th72:
  X is quasi-associative iff (for x,y being Element of X holds (x\y)`=(y\x)`)
proof
  thus X is quasi-associative implies
  (for x,y being Element of X holds (x\y)`=(y\x)`)
  proof
    assume X is quasi-associative;
    then for x being Element of X holds x`<=x by Th71;
    hence thesis by Lm16;
  end;
  assume for x,y being Element of X holds (x\y)`=(y\x)`;
  then for x,y being Element of X holds x`\y=(x\y)` by Lm17;
  then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm18;
  hence thesis by Lm19;
end;

theorem Th73:
  X is quasi-associative iff (for x,y being Element of X holds x`\y=(x\y)`)
proof
  thus X is quasi-associative
  implies (for x,y being Element of X holds x`\y=(x\y)`)
  proof
    assume X is quasi-associative;
    then for x,y being Element of X holds (x\y)`=(y\x)` by Th72;
    hence thesis by Lm17;
  end;
  assume for x,y being Element of X holds x`\y=(x\y)`;
  then for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X)by Lm18;
  hence thesis by Lm19;
end;

theorem
  X is quasi-associative
  iff (for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X))
proof
  thus X is quasi-associative
  implies (for x,y being Element of X holds (x\y)\(y\x) in BCK-part(X))
  proof
    assume X is quasi-associative;
    then for x,y being Element of X holds x`\y=(x\y)` by Th73;
    hence thesis by Lm18;
  end;
  thus thesis by Lm19;
end;

theorem
  X is quasi-associative
  iff (for x,y,z being Element of X holds (x\y)\z<=x\(y\z))
proof
  thus X is quasi-associative
  implies for x,y,z being Element of X holds (x\y)\z<=x\(y\z)
  proof
    assume X is quasi-associative;
    then for x being Element of X holds x`<=x by Th71;
    hence thesis by Lm20;
  end;
  assume for x,y,z being Element of X holds (x\y)\z<=x\(y\z);
  then for x being Element of X holds x`<=x by Lm20;
  hence thesis by Th71;
end;

begin :: Several Classes of BCI-algebra----alternative BCI-algebra

theorem Th76:
  X is alternative implies x` = x & x\(x\y) = y & (x\y)\y = x
proof
  assume
A1: X is alternative;
  thus x` = x
  proof x\(x\x) = (x\x)\x by A1,Def27;
    then x\0.X = (x\x)\x by Def5;
    then x\0.X = x` by Def5;
    hence thesis by Th2;
  end;
  thus x\(x\y) = y
  proof
    y\(y\y) = (y\y)\y by A1,Def27;
    then y\0.X = (y\y)\y by Def5;
    then y\0.X = y` by Def5;
    then
A2: y = y` by Th2;
    x\(x\y) = (x\x)\y by A1,Def27;
    hence thesis by A2,Def5;
  end;
  (x\y)\y=x\(y\y) by A1,Def27;
  then (x\y)\y=x\0.X by Def5;
  hence thesis by Th2;
end;

theorem
  X is alternative & x\a=x\b implies a=b
proof
  assume
A1: X is alternative & x\a=x\b;
  then (x\x)\a=x\(x\b) by Def27;
  then (x\x)\a=(x\x)\b by A1,Def27;
  then a`=(x\x)\b by Def5;
  then a`=b` by Def5;
  then a=b` by A1,Th76;
  hence thesis by A1,Th76;
end;

theorem
  X is alternative & a\x=b\x implies a=b
proof
  assume
A1: X is alternative & a\x=b\x;
  then a\(x\x)=(b\x)\x by Def27;
  then a\(x\x)=b\(x\x) by A1,Def27;
  then a\0.X=b\(x\x) by Def5;
  then a\0.X=b\0.X by Def5;
  then a=b\0.X by Th2;
  hence thesis by Th2;
end;

theorem
  X is alternative & x\y=0.X implies x=y
proof
  assume
A1: X is alternative & x\y=0.X;
  then x\(x\y)=x by Th2;
  then (x\x)\y=x by A1,Def27;
  then y`=x by Def5;
  hence thesis by A1,Th76;
end;

theorem
  X is alternative & (x\a)\b = 0.X implies a=x\b & b=x\a
proof
  assume
A1: X is alternative &(x\a)\b = 0.X;
  then (x\a)\(b\b) = b` by Def27;
  then (x\a)\0.X = b` by Def5;
  then x\a = b` by Th2;
  then x\(x\a) = x\b by A1,Th76;
  then (x\x)\a = x\b by A1,Def27;
  then a` = x\b by Def5;
  then a=x\b by A1,Th76;
  hence thesis by A1,Th76;
end;

Lm21: X is alternative iff X is associative
proof
  thus X is alternative implies X is associative
  proof
    assume
A1: X is alternative;
    for x,y,z being Element of X holds (x\y)\z = x\(y\z)
    proof
      let x,y,z be Element of X;
      ((x\y)\z)\(x\(y\z))=((x\y)\(x\(y\z)))\z by Th7;
      then ((x\y)\z)\(x\(y\z))=((x\(x\(y\z)))\y)\z by Th7;
      then ((x\y)\z)\(x\(y\z))=(((x\x)\(y\z))\y)\z by A1,Def27;
      then ((x\y)\z)\(x\(y\z))=(((y\z)`)\y)\z by Def5;
      then ((x\y)\z)\(x\(y\z))=((y\z)\y)\z by A1,Th76;
      then ((x\y)\z)\(x\(y\z))=((y\y)\z)\z by Th7;
      then ((x\y)\z)\(x\(y\z))=z`\z by Def5;
      then
A2:   ((x\y)\z)\(x\(y\z))=0.X by A1,Th76;
A3:   (x\(y\z))\((x\y)\z)=(((x\y)\y)\(y\z))\((x\y)\z) by A1,Th76
        .=(((x\y)\y)\((x\y)\z))\(y\z) by Th7;
      (((x\y)\y)\((x\y)\z))\(z\y)=0.X by Th1;
      then ((((x\y)\y)\((x\y)\z))\(y\z))\((z\y)\(y\z))=0.X by Th4;
      then ((((x\y)\y)\((x\y)\z))\(y\z))\((z\(y\z))\y)=0.X by Th7;
      then ((((x\y)\y)\((x\y)\z))\(y\z))\((z`\(y\z))\y)=0.X by A1,Th76;
      then ((((x\y)\y)\((x\y)\z))\(y\z))\((z`\(y\z))\y`)=0.X by A1,Th76;
      then ((((x\y)\y)\((x\y)\z))\(y\z))\0.X=0.X by Def3;
      then (x\(y\z))\((x\y)\z)=0.X by A3,Th2;
      hence thesis by A2,Def7;
    end;
    hence thesis by Def20;
  end;
  assume X is associative;
  then for x,y being Element of X holds x\(x\y) = (x\x)\y & (x\y)\y=x\(y\y)
  by Def20;
  hence thesis by Def27;
end;

Lm22: X is alternative implies X is implicative
proof
  assume X is alternative;
  then for x,y being Element of X holds (x\(x\y))\(y\x)=y\(y\x)by Th76;
  hence thesis by Def24;
end;

registration
  cluster alternative -> associative BCI-algebra;
  coherence by Lm21;
  cluster associative -> alternative BCI-algebra;
  coherence by Lm21;
  cluster alternative -> implicative BCI-algebra;
  coherence by Lm22;
end;

theorem
  X is alternative implies (x\(x\y))\(y\x) = x
proof
  assume
A1: X is alternative;
  then x\(x\y)=y by Th76;
  hence thesis by A1,Th76;
end;

theorem
  X is alternative implies y\(y\(x\(x\y))) = y
proof
  assume X is alternative;
  then y\(y\(x\(x\y)))=y\(y\y) by Th76
    .=y\0.X by Def5
    .= y by Th2;
  hence thesis;
end;

begin

:: Several Classes of BCI-algebra-
::-implicative & positive-implicative & weakly-positive-implicative BCI-algebra

Lm23: X is associative implies X is weakly-positive-implicative
proof
  assume
A1: X is associative;
  for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
  proof
    let x,y,z be Element of X;
    (x\y)\z=x\(y\z) by A1,Def20;
    then (x\y)\z=(x\0.X)\(y\z) by Th2;
    then (x\y)\z=(x\(z\z))\(y\z) by Def5;
    hence thesis by A1,Def20;
  end;
  hence thesis by Def23;
end;

Lm24: X is p-Semisimple BCI-algebra implies
X is weakly-positive-implicative BCI-algebra
proof
  assume
A1: X is p-Semisimple BCI-algebra;
  for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
  proof
    let x,y,z be Element of X;
    ((x\z)\z)\(y\z)=(x\z)\y by A1,Lm12
      .=(x\z)\(y\0.X) by Th2
      .=(x\y)\(z\0.X) by A1,Lm10;
    hence thesis by Th2;
  end;
  hence thesis by Def23;
end;

registration
  cluster associative -> weakly-positive-implicative BCI-algebra;
  coherence by Lm23;
  cluster p-Semisimple -> weakly-positive-implicative BCI-algebra;
  coherence by Lm24;
end;

theorem
  for X being non empty BCIStr_0 holds (X is implicative BCI-algebra
  iff (for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X
  & x\0.X=x &(x\(x\y))\(y\x)=y\(y\x)))
proof
  let X be non empty BCIStr_0;
  thus X is implicative BCI-algebra implies (for x,y,z being Element of X
  holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x & (x\(x\y))\(y\x)=y\(y\x))
  by Def24,Th1,Th2;
  thus (for x,y,z being Element of X holds
  ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x & (x\(x\y))\(y\x)=y\(y\x))
  implies X is implicative BCI-algebra
  proof
    assume
A1: for x,y,z being Element of X holds
    ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x &(x\(x\y))\(y\x)=y\(y\x);
A2: X is_I
    proof
      now
        let x be Element of X;
        x\x=(x\0.X)\x by A1
          .=(x\0.X)\(x\0.X) by A1
          .=((x\0.X)\(x\0.X))\0.X by A1
          .=((x\0.X)\(x\0.X))\(0.X)` by A1;
        hence x\x=0.X by A1;
      end;
      hence thesis by Def5;
    end;
A3: X is_BCI-4
    proof
      now
        let x,y be Element of X;
        assume
A4:     x\y = 0.X & y\x = 0.X;
        x=x\0.X by A1
          .=(y\(y\x))\(x\y) by A1,A4
          .=y\0.X by A1,A4;
        hence x=y by A1;
      end;
      hence thesis by Def7;
    end;
    now
      let x,y,z be Element of X;
      thus ((x\y)\(x\z))\(z\y)=0.X by A1;
      thus (x\(x\y))\y = 0.X
      proof
        (x\(x\y))\y=((x\0.X)\(x\y))\y by A1
          .=((x\0.X)\(x\y))\(y\0.X) by A1;
        hence thesis by A1;
      end;
    end;
    hence thesis by A1,A2,A3,Def24,Th1;
  end;
end;

theorem Th84:
  X is weakly-positive-implicative iff
  for x,y being Element of X holds x\y=((x\y)\y)\y`
proof
  thus X is weakly-positive-implicative implies
  for x,y being Element of X holds x\y=((x\y)\y)\y`
  proof
    assume
A1: X is weakly-positive-implicative;
    let x,y be Element of X;
    (x\0.X)\y=((x\y)\y)\y` by A1,Def23;
    hence thesis by Th2;
  end;
  assume
A2: for x,y being Element of X holds x\y=((x\y)\y)\y`;
  for x,y,z being Element of X holds (x\y)\z=((x\z)\z)\(y\z)
  proof
    let x,y,z be Element of X;
    ((x\z)\(y\z))\(x\y)=0.X by Def3;
    then (((x\z)\(y\z))\z)\((x\y)\z)=0.X by Th4;
    then
A3: (((x\z)\z)\(y\z))\((x\y)\z)=0.X by Th7;
A4: ((x\y)\z)\(((x\z)\z)\(y\z)) =((x\z)\y)\(((x\z)\z)\(y\z)) by Th7
      .=((((x\z)\z)\z`)\y)\(((x\z)\z)\(y\z)) by A2
      .=((((x\z)\z)\z`)\(((x\z)\z)\(y\z)))\y by Th7
      .=(((x\z)\z)\(((x\z)\z)\(y\z))\z`)\y by Th7;
    (((x\z)\z)\(((x\z)\z)\(y\z)))\(y\z)=0.X by Th1;
    then ((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\((y\z)\z`)=0.X by Th4;
    then (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\(((y\z)\z`)\y) =0.X by Th4;

then (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\(((y\z)\z`)\(y\0.X))=0.X by Th2;
    then (((((x\z)\z)\(((x\z)\z)\(y\z)))\z`)\y)\0.X=0.X by Def3;
    then ((x\y)\z)\(((x\z)\z)\(y\z))=0.X by A4,Th2;
    hence thesis by A3,Def7;
  end;
  hence thesis by Def23;
end;

Lm25: X is weakly-positive-implicative implies
(x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y)
proof
  assume
A1: X is weakly-positive-implicative;
  ((y\(y\x))\(y\x))\(x\(y\x))=0.X by Th1;
  then (((y\(y\x))\(y\x))\(x\y))\((x\(y\x))\(x\y))=0.X by Th4;
  then
A2: (((y\(y\x))\(y\x))\(x\y))\((x\(x\y))\(y\x))=0.X by Th7;
  ((x\(x\y))\(y\(x\y)))\(x\y)=0.X by Def3;
  then ((x\(x\y))\(x\y))\(y\(x\y))=0.X by Th7;
  then (((x\(x\y))\(x\y))\((x\y)`))\((y\(x\y))\((x\y)`))=0.X by Th4;
  then ((((x\(x\y))\(x\y))\((x\y)`))\(y\x))\(((y\(x\y))
  \((x\y)`))\(y\x))=0.X by Th4;
  then ((x\(x\y))\(y\x))\(((y\(x\y))\((x\y)`))\(y\x))=0.X by A1,Th84;
  then ((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\((x\y)`\(y\x)))
  =0.X by A1,Def23;
  then ((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\(((x\x)\(x\y))\(y\x)))
  =0.X by Def5;
  then ((x\(x\y))\(y\x))\((((y\(x\y))\(y\x))\(y\x))\0.X) =0.X by Th1;
  then ((x\(x\y))\(y\x))\(((y\(x\y))\(y\x))\(y\x)) =0.X by Th2;
  then ((x\(x\y))\(y\x))\(((y\(y\x))\(x\y))\(y\x)) =0.X by Th7;
  then ((x\(x\y))\(y\x))\(((y\(y\x))\(y\x))\(x\y))=0.X by Th7;
  hence thesis by A2,Def7;
end;

Lm26: X is positive-implicative iff X is weakly-positive-implicative
proof
  thus X is positive-implicative implies X is weakly-positive-implicative
  proof
    assume
A1: X is positive-implicative;
    for x,y being Element of X holds x\y=((x\y)\y)\y`
    proof
      let x,y be Element of X;
      ((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\((x\y)\(x\(x\(x\y)))) by A1,Def22;
      then ((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\((x\y)\(x\y)) by Th8;
      then ((x\y)\((x\y)\x))\(x\(x\y))=(x\y)\0.X by Def5;
      then ((x\y)\((x\y)\x))\(x\(x\y))=x\y by Th2;
      then ((x\y)\((x\x)\y))\(x\(x\y))=x\y by Th7;
      then ((x\y)\(x\(x\y)))\((x\x)\y)=x\y by Th7;
      then ((x\(x\(x\y)))\y)\((x\x)\y)=x\y by Th7;
      then ((x\y)\y)\((x\x)\y)=x\y by Th8;
      hence thesis by Def5;
    end;
    hence thesis by Th84;
  end;
  assume
A2: X is weakly-positive-implicative;
  for x,y being Element of X holds (x\(x\y))\(y\x)=x\(x\(y\(y\x)))
  proof
    let x,y be Element of X;
    (y\(y\x))\x = 0.X by Th1;
    then (x\x)\(x\(y\(y\x)))=0.X by Th4;
    then (x\(y\(y\x)))`=0.X by Def5;
    then x\(x\(y\(y\x)))=((x\(x\(y\(y\x))))\(x\(y\(y\x))))\0.X by A2,Th84;
    then x\(x\(y\(y\x)))=(x\(x\(y\(y\x))))\(x\(y\(y\x))) by Th2;
    then (x\(x\(y\(y\x))))\( (y\(y\x))\(x\(y\(y\x))) )=0.X by Th1;
    then ((x\(x\(y\(y\x)))))\(((y\(y\x))\(y\x))\(x\y))
    \(((y\(y\x))\(x\(y\(y\x))))\(((y\(y\x))\(y\x))\(x\y)))=0.X by Th4;
    then
A3: ((x\(x\(y\(y\x)))))\(((y\(y\x))\(y\x))\(x\y))
    \(((y\(y\x))\(((y\(y\x))\(y\x))\(x\y)))\(x\(y\(y\x))))=0.X by Th7;
A4: (x\(x\(y\(y\x)))) \ ((x\(x\y))\(y\x))
    =(x\(x\(y\(y\x)))) \ (((y\(y\x))\(y\x))\(x\y)) by A2,Lm25;
    ((y\(y\x))\(((y\(y\x))\(y\x))\(x\y)))\((x\y)\(y\x)`)
    =((((y\(y\x))\(y\x))\((y\x)`))\(((y\(y\x))\(y\x))\(x\y)))
    \((x\y)\((y\x)`)) by A2,Th84
      .=0.X by Th1;
    then (((y\(y\x))\(((y\(y\x))\(y\x))\(x\y)))\(x\(y\(y\x))))
    \(((x\y)\((y\x)`))\(x\(y\(y\x))))=0.X by Th4;
    then ((x\(x\(y\(y\x)))))\(((y\(y\x))\(y\x))\(x\y))
    \(((x\y)\((y\x)`))\(x\(y\(y\x))))=0.X by A3,Th3;
    then
A5: ((x\(x\(y\(y\x)))))\(((y\(y\x))\(y\x))\(x\y))
    \(((x\y)\(x\(y\(y\x))))\((y\x)`))=0.X by Th7;
    ((x\y)\(x\(y\(y\x))))\((y\(y\x))\y)=0.X by Th1;
    then ((x\y)\(x\(y\(y\x))))\((y\y)\(y\x))=0.X by Th7;
    then ((x\(x\(y\(y\x)))))\(((y\(y\x))\(y\x))\(x\y))\0.X=0.X by A5,Def5;
    then
A6: (x\(x\(y\(y\x))))\((x\(x\y))\(y\x))=0.X by A4,Th2;
    ((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X by Th10;
    hence thesis by A6,Def7;
  end;
  hence thesis by Def22;
end;

registration
  cluster positive-implicative -> weakly-positive-implicative BCI-algebra;
  coherence by Lm26;
  cluster alternative -> weakly-positive-implicative BCI-algebra;
  coherence;
end;

theorem
  X is weakly-positive-implicative BCI-algebra implies
  for x,y being Element of X holds (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y)
  by Lm25;

theorem
  for X being non empty BCIStr_0 holds (X is positive-implicative BCI-algebra
  iff (for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x
  & x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y)))
proof
  let X be non empty BCIStr_0;
  thus X is positive-implicative BCI-algebra implies
  (for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x
  & x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y))
  by Lm25,Th1,Th2,Th84;
  assume
A1: (for x,y,z being Element of X holds ((x\y)\(x\z))\(z\y)=0.X & x\0.X=x
  & x\y=((x\y)\y)\y` & (x\(x\y))\(y\x)=((y\(y\x))\(y\x))\(x\y));
A2: X is_I
  proof
    now
      let x be Element of X;
      ((x\0.X)\(x\0.X))\(0.X)`=0.X by A1;
      then ((x\0.X)\(x\0.X))\0.X=0.X by A1;
      then ((x\0.X)\x)\0.X=0.X by A1;
      then (x\x)\0.X=0.X by A1;
      hence x\x=0.X by A1;
    end;
    hence thesis by Def5;
  end;
A3: X is_BCI-4
  proof
    now
      let x,y be Element of X;
      assume x\y = 0.X & y\x = 0.X;
      then (x\0.X)\0.X=((y\0.X)\0.X)\0.X by A1;
      then (x\0.X)=((y\0.X)\0.X)\0.X by A1;
      then x=((y\0.X)\0.X)\0.X by A1;
      then x=(y\0.X)\0.X by A1;
      then x=y\0.X by A1;
      hence x=y by A1;
    end;
    hence thesis by Def7;
  end;
  now
    let x,y,z be Element of X;
    thus ((x\y)\(x\z))\(z\y)=0.X by A1;
    ((x\0.X)\(x\y))\(y\0.X)=0.X by A1;
    then (x\(x\y))\(y\0.X)=0.X by A1;
    hence (x\(x\y))\y = 0.X by A1;
  end;
  then X is weakly-positive-implicative BCI-algebra by A1,A2,A3,Th1,Th84;
  hence thesis by Lm26;
end;