:: Ideals of BCI-Algebras and Their Properties
::  by Chenglong Wu and Yuzhong Ding
::
:: Received March 3, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies BCIALG_1, XBOOLE_0, SUBSET_1, CARD_FIL, XXREAL_0, SUPINF_2,
      CHORD, TARSKI, RCOMP_1, BINOP_1, STRUCT_0, WAYBEL15, BCIIDEAL;
 notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
 constructors BCIALG_2, BCIALG_3;
 registrations STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
 requirements SUBSET, BOOLE;
 definitions BCIALG_1, TARSKI, XBOOLE_0;
 theorems BCIALG_1, TARSKI, XBOOLE_0, BCIALG_2, BCIALG_3;

begin :: Ideal of X

reserve X for BCI-algebra;
reserve X1 for non empty Subset of X;
reserve A,I for Ideal of X;
reserve x,y,z for Element of X;
reserve a for Element of A;

::P20

theorem
  for x,y,z,u being Element of X st x<=y holds u\(z\x)<=u\(z\y)
proof
  let x,y,z,u be Element of X;
  assume x<=y;
  then z\y<=z\x by BCIALG_1:5;
  hence thesis by BCIALG_1:5;
end;

theorem
  for x,y,z,u being Element of X holds (x\(y\z))\(x\(y\u))<=z\u
proof
  let x,y,z,u be Element of X;
  ((x\(y\z))\(x\(y\u)))\((y\u)\(y\z))=0.X by BCIALG_1:1;
  then ((x\(y\z))\(x\(y\u)))<=((y\u)\(y\z)) by BCIALG_1:def 11;
  then
A1: ((x\(y\z))\(x\(y\u)))\(z\u)<=((y\u)\(y\z))\(z\u) by BCIALG_1:5;
  ((y\u)\(y\z))\(z\u)=((y\u)\(z\u))\(y\z) by BCIALG_1:7;
  then ((x\(y\z))\(x\(y\u)))\(z\u)<=0.X by A1,BCIALG_1:def 3;
  then ((x\(y\z))\(x\(y\u)))\(z\u)\0.X=0.X by BCIALG_1:def 11;
  then ((x\(y\z))\(x\(y\u)))\(z\u)=0.X by BCIALG_1:2;
  hence thesis by BCIALG_1:def 11;
end;

theorem
  for x,y,z,u,v being Element of X holds (x\(y\(z\u)))\(x\(y\(z\v)))<=v\ u
proof
  let x,y,z,u,v be Element of X;
  (x\(y\(z\u)))\(x\(y\(z\v)))\((y\(z\v))\(y\(z\u)))=0.X by BCIALG_1:1;
  then (x\(y\(z\u)))\(x\(y\(z\v))) <=((y\(z\v))\(y\(z\u))) by BCIALG_1:def 11;
  then
A1: (x\(y\(z\u)))\(x\(y\(z\v)))\((z\u)\(z\v)) <=((y\(z\v))\(y\(z\u)))\((z\u)\
  (z\v)) by BCIALG_1:5;
  ((y\(z\v))\(y\(z\u)))\((z\u)\(z\v))=((y\(z\v))\((z\u)\(z\v)))\(y\(z\u))
  by BCIALG_1:7;
  then (x\(y\(z\u)))\(x\(y\(z\v)))\((z\u)\(z\v))<=0.X by A1,BCIALG_1:def 3;
  then (x\(y\(z\u)))\(x\(y\(z\v)))\((z\u)\(z\v))\0.X=0.X by BCIALG_1:def 11;
  then (x\(y\(z\u)))\(x\(y\(z\v)))\((z\u)\(z\v))=0.X by BCIALG_1:2;
  then (x\(y\(z\u)))\(x\(y\(z\v))) <= (z\u)\(z\v) by BCIALG_1:def 11;
  then
A2: (x\(y\(z\u)))\(x\(y\(z\v)))\(v\u)<= ((z\u)\(z\v))\(v\u) by BCIALG_1:5;
  ((z\u)\(z\v))\(v\u)=((z\u)\(v\u))\(z\v) by BCIALG_1:7
    .=0.X by BCIALG_1:def 3;
  then (x\(y\(z\u)))\(x\(y\(z\v)))\(v\u)\0.X=0.X by A2,BCIALG_1:def 11;
  then (x\(y\(z\u)))\(x\(y\(z\v)))\(v\u)=0.X by BCIALG_1:2;
  hence thesis by BCIALG_1:def 11;
end;

theorem
  for x,y being Element of X holds (0.X\(x\y))\(y\x)=0.X
proof
  let x,y be Element of X;
  ((0.X\x)\(0.X\y))\(y\x)=((0.X\x)\(y\x))\(0.X\y) by BCIALG_1:7;
  then
A1: ((0.X\x)\(0.X\y))\(y\x)=(((y\x)`)\x)\(0.X\y) by BCIALG_1:7
    .=(((y`\x`))\x)\(0.X\y) by BCIALG_1:9
    .=(((y`\x))\x`)\(0.X\y) by BCIALG_1:7
    .=(((y`\x))\y`)\x` by BCIALG_1:7
    .=(((y`\y`))\x)\x` by BCIALG_1:7
    .=x`\x` by BCIALG_1:def 5
    .=0.X by BCIALG_1:def 5;
  (0.X\(x\y))\(y\x)=((x\y)`)\(y\x) .=(x`\y`)\(y\x) by BCIALG_1:9
    .=((0.X\x)\(0.X\y))\(y\x);
  hence thesis by A1;
end;

::P26

definition
  let X;
  let a be Element of X;
  func initial_section(a) equals
  {x where x is Element of X:x<=a};
  coherence;
end;

theorem Th5: ::proposition 1.4.1
  x<=a implies x in A
proof
  assume x<=a;
  then x\a = 0.X by BCIALG_1:def 11;
  then x\a in A by BCIALG_1:def 18;
  hence thesis by BCIALG_1:def 18;
end;

::P37

theorem
  for x,a,b being Element of AtomSet(X) holds x is Element of BranchV(b)
  implies a\x=a\b
proof
  set P = AtomSet(X);
  let x,a,b be Element of P;
  set B = BranchV(b);
  assume x is Element of B;
  then x in B;
  then ex x3 being Element of X st x=x3 & b<=x3;
  then
A1: b\x=0.X by BCIALG_1:def 11;
  x in {x1 where x1 is Element of X:x1 is minimal};
  then ex x1 being Element of X st x=x1 & x1 is minimal;
  hence thesis by A1,BCIALG_1:def 14;
end;

theorem
  for a being Element of X,x,b being Element of AtomSet(X) holds x is
  Element of BranchV(b) implies a\x=a\b
proof
  set P = AtomSet(X);
  let a be Element of X;
  let x,b be Element of P;
  set B = BranchV(b);
  assume x is Element of B;
  then x in B;
  then ex x3 being Element of X st x=x3 & b<=x3;
  then
A1: b\x=0.X by BCIALG_1:def 11;
  x in {x1 where x1 is Element of X:x1 is minimal};
  then ex x1 being Element of X st x=x1 & x1 is minimal;
  hence thesis by A1,BCIALG_1:def 14;
end;

theorem
  initial_section(a) c= A
proof
  let b be set;
  assume b in initial_section(a);
  then ex x1 being Element of X st b=x1 & x1<=a;
  hence thesis by Th5;
end;

theorem
  AtomSet(X) is Ideal of X implies for x being Element of BCK-part(X),a
  being Element of AtomSet(X) st x\a in AtomSet(X) holds x=0.X
proof
  set B = BCK-part(X);
  set P = AtomSet(X);
A1: x in {0.X} iff x in B/\P
  proof
    0.X in B & 0.X in P by BCIALG_1:19;
    then 0.X in B/\P by XBOOLE_0:def 4;
    hence x in {0.X} implies x in B/\P by TARSKI:def 1;
    thus x in B/\P implies x in {0.X}
    proof
      assume
A2:   x in B/\P;
      then x in B by XBOOLE_0:def 4;
      then ex x1 being Element of X st x=x1 & 0.X<=x1;
      then
A3:   0.X\x=0.X by BCIALG_1:def 11;
      x in {x2 where x2 is Element of X:x2 is minimal} by A2,XBOOLE_0:def 4;
      then ex x2 being Element of X st x=x2 & x2 is minimal;
      then 0.X=x by A3,BCIALG_1:def 14;
      hence thesis by TARSKI:def 1;
    end;
  end;
  assume
A4: P is Ideal of X;
  for x being Element of B,a being Element of P st x\a in P holds x=0.X
  proof
    let x be Element of B;
    let a be Element of P;
    assume x\a in P;
    then x in P by A4,BCIALG_1:def 18;
    then x in B /\ P by XBOOLE_0:def 4;
    then x in {0.X} by A1;
    hence thesis by TARSKI:def 1;
  end;
  hence thesis;
end;

theorem
  AtomSet(X) is Ideal of X implies AtomSet(X) is closed Ideal of X
proof
  set P = AtomSet(X);
A1: for x being Element of P holds x` in P
  proof
    let x be Element of P;
    x` is minimal by BCIALG_2:30;
    hence thesis;
  end;
  assume P is Ideal of X;
  hence thesis by A1,BCIALG_1:def 19;
end;

::p47

definition
  let X,I;
  attr I is positive means
  for x being Element of I holds x is positive;
end;

::P48

theorem
  for X being BCK-algebra,A,I being Ideal of X holds (A/\I={0.X} iff for
  x being Element of A,y being Element of I holds x\y =x )
proof
  let X be BCK-algebra;
  let A,I be Ideal of X;
  thus A/\I={0.X} implies for x being Element of A,y being Element of I holds
  x\y =x
  proof
    assume
A1: A/\I={0.X};
    let x be Element of A;
    let y be Element of I;
    x\(x\y)\y=0.X by BCIALG_1:1;
    then x\(x\y)<=y by BCIALG_1:def 11;
    then
A2: x\(x\y) in I by Th5;
    (x\(x\y))\x = x\x\(x\y) by BCIALG_1:7
      .=(x\y)` by BCIALG_1:def 5
      .=0.X by BCIALG_1:def 8;
    then (x\(x\y))<=x by BCIALG_1:def 11;
    then x\(x\y) in A by Th5;
    then x\(x\y) in {0.X} by A1,A2,XBOOLE_0:def 4;
    then
A3: x\(x\y)=0.X by TARSKI:def 1;
    (x\y)\x = x\x\y by BCIALG_1:7
      .=y` by BCIALG_1:def 5
      .=0.X by BCIALG_1:def 8;
    hence thesis by A3,BCIALG_1:def 7;
  end;
  thus (for x being Element of A,y being Element of I holds x\y =x) implies A
  /\I={0.X}
  proof
    assume
A4: for x being Element of A,y being Element of I holds x\y =x;
    thus A/\I c= {0.X}
    proof
      let x be set;
      assume
A5:   x in A/\I;
      then reconsider xxx=x as Element of A by XBOOLE_0:def 4;
      reconsider xx=x as Element of I by A5,XBOOLE_0:def 4;
      xxx\xx=xxx by A4;
      then x=0.X by BCIALG_1:def 5;
      hence thesis by TARSKI:def 1;
    end;
    let x be set;
    assume x in {0.X};
    then
A6: x =0.X by TARSKI:def 1;
    0.X in A & 0.X in I by BCIALG_1:def 18;
    hence thesis by A6,XBOOLE_0:def 4;
  end;
end;

::P50

theorem
  for X being associative BCI-algebra,A being Ideal of X holds A is closed
proof
  let X be associative BCI-algebra;
  let A be Ideal of X;
  for x being Element of A holds x` in A
  proof
    let x be Element of A;
    0.X\x=x\0.X by BCIALG_1:48
      .=x by BCIALG_1:2;
    hence thesis;
  end;
  hence thesis by BCIALG_1:def 19;
end;

theorem
  for X being BCI-algebra,A being Ideal of X st X is quasi-associative
  holds A is closed
proof
  let X be BCI-algebra;
  let A be Ideal of X;
  assume
A1: X is quasi-associative;
  for x being Element of A holds x` in A
  proof
    let x be Element of A;
    x`<=x by A1,BCIALG_1:71;
    hence thesis by Th5;
  end;
  hence thesis by BCIALG_1:def 19;
end;

begin :: associative  Ideal of X

definition
  let X be BCI-algebra,IT be Ideal of X;
  attr IT is associative means
  :Def3:
  0.X in IT & for x,y,z being Element of X
  st x\(y\z) in IT & y\z in IT holds x in IT;
end;

registration
  let X be BCI-algebra;
  cluster associative for Ideal of X;
  existence
  proof
    take Y={0.X};
    reconsider YY=Y as Ideal of X by BCIALG_1:43;
A1: 0.X in YY by TARSKI:def 1;
    for x,y,z being Element of X st x\(y\z) in YY & y\z in YY holds x=0.X
    proof
      let x,y,z be Element of X;
      assume x\(y\z) in YY & y\z in YY;
      then x\(y\z)=0.X & y\z=0.X by TARSKI:def 1;
      hence thesis by BCIALG_1:2;
    end;
    then
    for x,y,z being Element of X st x\(y\z) in YY&y\z in YY holds x in YY
    by A1;
    hence thesis by A1,Def3;
  end;
end;

definition
  let X be BCI-algebra;
  mode associative-ideal of X -> non empty Subset of X means
    :Def4:
    0.X in it
    & for x,y,z being Element of X st (x\y)\z in it & y\z in it holds x in it;
  existence
  proof
    take X1=the carrier of X;
    X1 c= the carrier of X;
    hence thesis;
  end;
end;

theorem
  X1 is associative-ideal of X implies X1 is Ideal of X
proof
  assume
A1: X1 is associative-ideal of X;
A2: 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 in X1 & y\0.X in X1 by BCIALG_1:2;
    hence thesis by A1,Def4;
  end;
  0.X in X1 by A1,Def4;
  hence thesis by A2,BCIALG_1:def 18;
end;

theorem Th15:
  I is associative-ideal of X iff for x,y,z st (x\y)\z in I holds x\(y\z) in I
proof
  thus I is associative-ideal of X implies for x,y,z st (x\y)\z in I holds x\(
  y\z) in I
  proof
    assume
A1: I is associative-ideal of X;
    let x,y,z such that
A2: (x\y)\z in I;
    x\(x\y)\y =0.X by BCIALG_1:1;
    then x\(x\y)<= y by BCIALG_1:def 11;
    then x\(x\y)\(y\z)<= y\(y\z) by BCIALG_1:5;
    then
A3: (x\(x\y)\(y\z))\z <= (y\(y\z))\z by BCIALG_1:5;
    (y\(y\z))\z =0.X by BCIALG_1:1;
    then ((x\(x\y)\(y\z))\z)\0.X=0.X by A3,BCIALG_1:def 11;
    then ((x\(x\y))\(y\z))\z =0.X by BCIALG_1:2;
    then ((x\(x\y))\(y\z))\z in I by A1,Def4;
    then ((x\(y\z))\(x\y))\z in I by BCIALG_1:7;
    hence thesis by A1,A2,Def4;
  end;
  assume
A4: for x,y,z st (x\y)\z in I holds x\(y\z) in I;
A5: for x,y,z st (x\y)\z in I & y\z in I holds x in I
  proof
    let x,y,z such that
A6: (x\y)\z in I and
A7: y\z in I;
    x\(y\z) in I by A4,A6;
    hence thesis by A7,BCIALG_1:def 18;
  end;
  0.X in I by BCIALG_1:def 18;
  hence thesis by A5,Def4;
end;

theorem
  I is associative-ideal of X implies for x being Element of X holds x\(
  0.X\x) in I
proof
  assume
A1: I is associative-ideal of X;
  let x be Element of X;
  x\x = 0.X by BCIALG_1:def 5;
  then
A2: (x\0.X)\x =0.X by BCIALG_1:2;
  0.X in I by A1,Def4;
  hence thesis by A1,A2,Th15;
end;

theorem
  (for x being Element of X holds x\(0.X\x) in I) implies I is closed
  Ideal of X
proof
  assume
A1: for x being Element of X holds x\(0.X\x) in I;
  for x1 being Element of I holds x1` in I
  proof
    let x1 be Element of I;
    (0.X\x1)\x1=(0.X\(0.X\(0.X\x1)))\x1 by BCIALG_1:8;
    then (0.X\x1)\x1=(0.X\x1)\(0.X\(0.X\x1)) by BCIALG_1:7;
    then (0.X\x1)\x1 in I by A1;
    hence thesis by BCIALG_1:def 18;
  end;
  hence thesis by BCIALG_1:def 19;
end;

definition
  let X be BCI-algebra;
  mode p-ideal of X -> non empty Subset of X means
    :Def5:
    0.X in it & for x,y,
    z being Element of X st (x\z)\(y\z) in it & y in it holds x in it;
  existence
  proof
    take X1=the carrier of X;
    X1 c= X1;
    hence thesis;
  end;
end;

theorem
  X1 is p-ideal of X implies X1 is Ideal of X
proof
  assume
A1: X1 is p-ideal of X;
A2: 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 that
A3: x\y in X1 and
A4: y in X1;
    (x\0.X)\y in X1 by A3,BCIALG_1:2;
    then (x\0.X)\(y\0.X) in X1 by BCIALG_1:2;
    hence thesis by A1,A4,Def5;
  end;
  0.X in X1 by A1,Def5;
  hence thesis by A2,BCIALG_1:def 18;
end;

theorem Th19:
  for X,I st I is p-ideal of X holds BCK-part(X) c= I
proof
  let X,I;
  assume
A1: I is p-ideal of X;
  let x be set;
  assume
A2: x in BCK-part(X);
  then
A3: ex x1 being Element of X st x=x1 & 0.X<=x1;
  reconsider x as Element of X by A2;
  0.X\x = 0.X by A3,BCIALG_1:def 11;
  then 0.X\(0.X\x)=0.X by BCIALG_1:2;
  then
A4: (x\x)\(0.X\x)=0.X by BCIALG_1:def 5;
  0.X in I by A1,Def5;
  hence thesis by A1,A4,Def5;
end;

theorem
  BCK-part(X) is p-ideal of X
proof
  set A = BCK-part(X);
A1: now
    let x,y,z be Element of X;
    assume that
A2: (x\z)\(y\z) in A and
A3: y in A;
    ex c being Element of X st (x\z)\(y\z) = c & 0.X<=c by A2;
    then ((x\z)\(y\z))`= 0.X by BCIALG_1:def 11;
    then ((x\z)`)\((y\z)`)=0.X by BCIALG_1:9;
    then
A4: (x`\z`)\((y\z)`)=0.X by BCIALG_1:9;
    ex d being Element of X st y=d & 0.X<=d by A3;
    then y` = 0.X by BCIALG_1:def 11;
    then ((x`\z`)\(0.X\z`))\(x`\0.X)=(x`\0.X)` by A4,BCIALG_1:9;
    then ((x`\z`)\(0.X\z`))\(x`\0.X)=x`` by BCIALG_1:2;
    then 0.X = 0.X\(0.X\x) by BCIALG_1:def 3;
    then 0.X\x = 0.X by BCIALG_1:1;
    then 0.X <= x by BCIALG_1:def 11;
    hence x in A;
  end;
  0.X\0.X=0.X by BCIALG_1:def 5;
  then 0.X <= 0.X by BCIALG_1:def 11;
  then 0.X in A;
  hence thesis by A1,Def5;
end;

theorem Th21:
  I is p-ideal of X iff for x,y st x in I & x<=y holds y in I
proof
  thus I is p-ideal of X implies for x,y st x in I & x<=y holds y in I
  proof
    assume I is p-ideal of X;
    then
A1: BCK-part(X) c= I by Th19;
    let x,y such that
A2: x in I and
A3: x <= y;
A4: x\y = 0.X by A3,BCIALG_1:def 11;
    then (y\x)`=x\y by BCIALG_1:6;
    then 0.X <= y\x by A4,BCIALG_1:def 11;
    then y\x in BCK-part(X);
    hence thesis by A2,A1,BCIALG_1:def 18;
  end;
  assume
A5: for x,y st x in I & x<=y holds y in I;
A6: for x,y,z st (x\z)\(y\z) in I & y in I holds x in I
  proof
    let x,y,z such that
A7: (x\z)\(y\z) in I and
A8: y in I;
    ((x\z)\(y\z))\(x\y)=0.X by BCIALG_1:def 3;
    then ((x\z)\(y\z))<= x\y by BCIALG_1:def 11;
    then x\y in I by A5,A7;
    hence thesis by A8,BCIALG_1:def 18;
  end;
  0.X in I by BCIALG_1:def 18;
  hence thesis by A6,Def5;
end;

theorem
  I is p-ideal of X iff for x,y,z st (x\z)\(y\z) in I holds x\y in I
proof
  thus I is p-ideal of X implies for x,y,z st (x\z)\(y\z) in I holds x\y in I
  proof
    assume
A1: I is p-ideal of X;
    let x,y,z such that
A2: (x\z)\(y\z) in I;
    (x\z)\(y\z)\(x\y) = 0.X by BCIALG_1:def 3;
    then (x\z)\(y\z) <= (x\y) by BCIALG_1:def 11;
    hence thesis by A1,A2,Th21;
  end;
  assume
A3: for x,y,z st (x\z)\(y\z) in I holds x\y in I;
A4: for x,y,z st (x\z)\(y\z) in I & y in I holds x in I
  proof
    let x,y,z such that
A5: (x\z)\(y\z) in I and
A6: y in I;
    x\y in I by A3,A5;
    hence thesis by A6,BCIALG_1:def 18;
  end;
  0.X in I by BCIALG_1:def 18;
  hence thesis by A4,Def5;
end;

begin :: P132: commutative Ideal of X

definition
  let X be BCK-algebra, IT be Ideal of X;
  attr IT is commutative means
  :Def6:
  for x,y,z being Element of X st (x\y)\z
  in IT & z in IT holds x\(y\(y\x)) in IT;
end;

registration
  let X be BCK-algebra;
  cluster commutative for Ideal of X;
  existence
  proof
    set X1 = BCK-part(X);
    take X1;
A1: 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 and
A3:   y in X1;
      ex x2 being Element of X st y=x2 & 0.X<=x2 by A3;
      then
A4:   y`=0.X by BCIALG_1:def 11;
      ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
      then (x\y)`=0.X by BCIALG_1:def 11;
      then x`\0.X = 0.X by A4,BCIALG_1:9;
      then 0.X\x=0.X by BCIALG_1:2;
      then 0.X<= x by BCIALG_1:def 11;
      hence thesis;
    end;
A5: for x,y,z being Element of X st (x\y)\z in X1 & z in X1 holds x\(y\(y
    \x)) in X1
    proof
      let x,y,z be Element of X;
      assume that
      (x\y)\z in X1 and
      z in X1;
      0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
      then 0.X <= (x\(y\(y\x))) by BCIALG_1:def 11;
      hence thesis;
    end;
    0.X in BCK-part(X) by BCIALG_1:19;
    then X1 is Ideal of X by A1,BCIALG_1:def 18;
    hence thesis by A5,Def6;
  end;
end;

theorem
  for X being BCK-algebra holds BCK-part(X) is commutative Ideal of X
proof
  let X be BCK-algebra;
  set B = BCK-part(X);
A1: for x,y being Element of X st x\y in B & y in B holds x in B
  proof
    let x,y be Element of X such that
A2: x\y in B and
A3: y in B;
    ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
    then (x\y)`=0.X by BCIALG_1:def 11;
    then
A4: x`\y`=0.X by BCIALG_1:9;
    ex x2 being Element of X st y=x2 & 0.X<=x2 by A3;
    then x`\0.X = 0.X by A4,BCIALG_1:def 11;
    then 0.X\x=0.X by BCIALG_1:2;
    then 0.X<= x by BCIALG_1:def 11;
    hence thesis;
  end;
A5: for x,y,z being Element of X st (x\y)\z in B & z in B holds x\(y\(y\x))
  in B
  proof
    let x,y,z be Element of X;
    assume that
    (x\y)\z in B and
    z in B;
    0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
    then 0.X <= (x\(y\(y\x))) by BCIALG_1:def 11;
    hence thesis;
  end;
  0.X in BCK-part(X) by BCIALG_1:19;
  hence thesis by A1,A5,Def6,BCIALG_1:def 18;
end;

theorem
  for X being BCK-algebra st X is p-Semisimple BCI-algebra holds {0.X}
  is commutative Ideal of X
proof
  let X be BCK-algebra;
  set X1={0.X};
A1: X1 c= the carrier of X
  proof
    let xx be set;
    assume xx in X1;
    then xx=0.X by TARSKI:def 1;
    hence thesis;
  end;
A2: for x,y being Element of X st x\y in {0.X} & y in {0.X} holds x in {0.X}
  proof
    set X1={0.X};
    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 BCIALG_1:2;
    hence thesis by TARSKI:def 1;
  end;
  0.X in {0.X} by TARSKI:def 1;
  then reconsider X1 as Ideal of X by A1,A2,BCIALG_1:def 18;
  assume
A3: X is p-Semisimple BCI-algebra;
  for x,y,z being Element of X st (x\y)\z in X1 & z in X1 holds x\(y\(y\x
  )) in X1
  proof
    let x,y,z be Element of X;
    assume (x\y)\z in X1 & z in X1;
    then (x\y)\z=0.X & z=0.X by TARSKI:def 1;
    then
A4: x\y = 0.X by BCIALG_1:2;
    y is atom by A3,BCIALG_1:52;
    then x=y by A4,BCIALG_1:def 14;
    then x\(y\(y\x))=x\(x\(0.X)) by BCIALG_1:def 5;
    then x\(y\(y\x))=x\x by BCIALG_1:2;
    then x\(y\(y\x))=0.X by BCIALG_1:def 5;
    hence thesis by TARSKI:def 1;
  end;
  hence thesis by Def6;
end;

Lm1: for X being BCK-algebra holds the carrier of X c= BCK-part(X)
proof
  let X be BCK-algebra;
  let x be set;
  assume x in the carrier of X;
  then consider x1 being Element of X such that
A1: x=x1;
  x1` = 0.X by BCIALG_1:def 8;
  then 0.X <= x1 by BCIALG_1:def 11;
  hence thesis by A1;
end;

reserve X for BCK-algebra;

theorem Th25:
  BCK-part(X) = the carrier of X
proof
  the carrier of X c= BCK-part(X) by Lm1;
  hence thesis by XBOOLE_0:def 10;
end;

reserve X for BCI-algebra;

theorem
  (for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y)
  implies the carrier of X = BCK-part(X)
proof
  assume for X being BCI-algebra,x,y being Element of X holds (x\y)\y=x\y;
  then X is BCK-algebra by BCIALG_1:13;
  hence thesis by Th25;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x)
  implies the carrier of X = BCK-part(X)
proof
  assume for X being BCI-algebra,x,y being Element of X holds x\(y\x)=x;
  then X is BCK-algebra by BCIALG_1:14;
  hence thesis by Th25;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x))
  implies the carrier of X = BCK-part(X)
proof
  assume for X being BCI-algebra,x,y being Element of X holds x\(x\y)=y\(y\x);
  then X is BCK-algebra by BCIALG_1:12;
  hence thesis by Th25;
end;

theorem
  (for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z)\
  (y\z)) implies the carrier of X = BCK-part(X)
proof
  assume
  for X being BCI-algebra,x,y,z being Element of X holds (x\y)\y=(x\z) \(y\z);
  then X is BCK-algebra by BCIALG_1:15;
  hence thesis by Th25;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y)
  implies the carrier of X = BCK-part(X)
proof
  assume for X being BCI-algebra,x,y being Element of X holds (x\y)\(y\x)=x\y;
  then X is BCK-algebra by BCIALG_1:16;
  hence thesis by Th25;
end;

theorem
  (for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y\
  x))=0.X) implies the carrier of X = BCK-part(X)
proof
  assume for X being BCI-algebra,x,y being Element of X holds (x\y)\((x\y)\(y
  \x))=0.X;
  then X is BCK-algebra by BCIALG_1:17;
  hence thesis by Th25;
end;

theorem
  for X being BCK-algebra holds the carrier of X is commutative Ideal of X
proof
  let X be BCK-algebra;
  set B = BCK-part(X);
A1: for x,y being Element of X st x\y in B & y in B holds x in B
  proof
    let x,y be Element of X such that
A2: x\y in B and
A3: y in B;
    ex x1 being Element of X st x\y=x1 & 0.X<=x1 by A2;
    then (x\y)`=0.X by BCIALG_1:def 11;
    then
A4: x`\y`=0.X by BCIALG_1:9;
    ex x2 being Element of X st y=x2 & 0.X<=x2 by A3;
    then x`\0.X = 0.X by A4,BCIALG_1:def 11;
    then 0.X\x=0.X by BCIALG_1:2;
    then 0.X<= x by BCIALG_1:def 11;
    hence thesis;
  end;
A5: for x,y,z being Element of X st (x\y)\z in B & z in B holds x\(y\(y\x))
  in B
  proof
    let x,y,z be Element of X;
    assume that
    (x\y)\z in B and
    z in B;
    0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8;
    then 0.X <= (x\(y\(y\x))) by BCIALG_1:def 11;
    hence thesis;
  end;
  the carrier of X=B by Th25;
  hence thesis by A1,A5,Def6,BCIALG_1:def 18;
end;

reserve X for BCK-algebra;
reserve I for Ideal of X;

theorem Th33:
  I is commutative Ideal of X iff for x,y being Element of X st x\
  y in I holds x\(y\(y\x)) in I
proof
  thus I is commutative Ideal of X implies for x,y being Element of X st x\y
  in I holds x\(y\(y\x)) in I
  proof
A1: 0.X in I by BCIALG_1:def 18;
    assume
A2: I is commutative Ideal of X;
    let x,y be Element of X;
    assume x\y in I;
    then (x\y)\0.X in I by BCIALG_1:2;
    hence thesis by A2,A1,Def6;
  end;
  assume
A3: for x,y being Element of X st x\y in I holds x\(y\(y\x)) in I;
  for x,y,z being Element of X st (x\y)\z in I & z in I holds x\(y\(y\x)) in I
  proof
    let x,y,z be Element of X;
    assume (x\y)\z in I & z in I;
    then x\y in I by BCIALG_1:def 18;
    hence thesis by A3;
  end;
  hence thesis by Def6;
end;

theorem Th34:
  for I,A being Ideal of X st I c= A & I is commutative Ideal of X
  holds A is commutative Ideal of X
proof
  let I,A be Ideal of X;
  assume that
A1: I c= A and
A2: I is commutative Ideal of X;
  for x,y being Element of X st x\y in A holds x\(y\(y\x)) in A
  proof
    let x,y be Element of X;
A3: for x,y,z,u being Element of X st x<=y holds u\(z\x)<=u\(z\y)
    proof
      let x,y,z,u be Element of X;
      assume x<=y;
      then z\y<=z\x by BCIALG_1:5;
      hence thesis by BCIALG_1:5;
    end;
    (x\(x\y))\x=(x\x)\(x\y) by BCIALG_1:7
      .= (x\y)` by BCIALG_1:def 5
      .= 0.X by BCIALG_1:def 8;
    then x\(x\y)<=x by BCIALG_1:def 11;
    then y\(y\(x\(x\y)))<=y\(y\x) by A3;
    then
A4: x\(y\(y\x))<=x\(y\(y\(x\(x\y)))) by BCIALG_1:5;
    (x\(x\y))\y=(x\y)\(x\y) by BCIALG_1:7
      .=0.X by BCIALG_1:def 5;
    then (x\(x\y))\y in I by BCIALG_1:def 18;
    then (x\(x\y))\(y\(y\(x\(x\y)))) in I by A2,Th33;
    then (x\(x\y))\(y\(y\(x\(x\y)))) in A by A1;
    then
A5: (x\(y\(y\(x\(x\y)))))\(x\y) in A by BCIALG_1:7;
    assume x\y in A;
    then (x\(y\(y\(x\(x\y))))) in A by A5,BCIALG_1:def 18;
    hence thesis by A4,Th5;
  end;
  hence thesis by Th33;
end;

theorem Th35:
  (for I being Ideal of X holds I is commutative Ideal of X) iff {
  0.X} is commutative Ideal of X
proof
  thus (for I being Ideal of X holds I is commutative Ideal of X) implies {0.X
  } is commutative Ideal of X by BCIALG_1:43;
  thus {0.X} is commutative Ideal of X implies for I being Ideal of X holds I
  is commutative Ideal of X
  proof
    assume
A1: {0.X} is commutative Ideal of X;
    let I be Ideal of X;
    for I being Ideal of X holds {0.X} c= I
    proof
      let I be Ideal of X;
      let x be set;
      assume x in {0.X};
      then x=0.X by TARSKI:def 1;
      hence thesis by BCIALG_1:def 18;
    end;
    hence thesis by A1,Th34;
  end;
end;

theorem Th36:
  {0.X} is commutative Ideal of X iff X is commutative BCK-algebra
proof
A1: X is commutative BCK-algebra implies for x,y being Element of X holds x\y
  = x\(y\(y\x))
  proof
    assume
A2: X is commutative BCK-algebra;
    let x,y be Element of X;
    x\y = x\(x\(x\y)) by BCIALG_1:8
      .= x\(y\(y\x)) by A2,BCIALG_3:def 1;
    hence thesis;
  end;
  thus {0.X} is commutative Ideal of X implies X is commutative BCK-algebra
  proof
    assume
A3: {0.X} is commutative Ideal of X;
    for x,y being Element of X st x<=y holds x=y\(y\x)
    proof
      let x,y be Element of X;
      assume x<=y;
      then x\y=0.X by BCIALG_1:def 11;
      then x\y in {0.X} by TARSKI:def 1;
      then x\(y\(y\x)) in {0.X} by A3,Th33;
      then (y\(y\x))\x=0.X & x\(y\(y\x))=0.X by BCIALG_1:1,TARSKI:def 1;
      hence thesis by BCIALG_1:def 7;
    end;
    hence thesis by BCIALG_3:5;
  end;
  assume X is commutative BCK-algebra;
  then for x,y being Element of X st x\y in {0.X} holds x\(y\(y\x)) in {0.X}
  by A1;
  hence thesis by Th33,BCIALG_1:43;
end;

theorem Th37:
  X is commutative BCK-algebra iff for I being Ideal of X holds I
  is commutative Ideal of X
proof
  thus X is commutative BCK-algebra implies for I being Ideal of X holds I is
  commutative Ideal of X
  proof
    assume X is commutative BCK-algebra;
    then {0.X} is commutative Ideal of X by Th36;
    hence thesis by Th35;
  end;
  assume for I being Ideal of X holds I is commutative Ideal of X;
  then {0.X} is commutative Ideal of X by Th35;
  hence thesis by Th36;
end;

theorem
  {0.X} is commutative Ideal of X iff for I being Ideal of X holds I is
  commutative Ideal of X
proof
  thus {0.X} is commutative Ideal of X implies for I being Ideal of X holds I
  is commutative Ideal of X
  proof
    assume {0.X} is commutative Ideal of X;
    then X is commutative BCK-algebra by Th36;
    hence thesis by Th37;
  end;
  assume for I being Ideal of X holds I is commutative Ideal of X;
  then X is commutative BCK-algebra by Th37;
  hence thesis by Th36;
end;

reserve I for Ideal of X;

theorem
  for x,y being Element of X holds x\(x\y) in I implies x\((x\y)\((x\y)\
  x)) in I & (y\(y\x))\x in I & y\(y\x)\(x\y) in I
proof
  let x,y be Element of X;
  assume
A1: x\(x\y) in I;
  (x\y)\((x\y)\x)=(x\y)\((x\x)\y) by BCIALG_1:7
    .=(x\((x\x)\y))\y by BCIALG_1:7
    .=(x\y`)\y by BCIALG_1:def 5
    .=(x\0.X)\y by BCIALG_1:def 8
    .=x\y by BCIALG_1:2;
  hence x\((x\y)\((x\y)\x)) in I by A1;
  (y\0.X)\(y\x)\(x\0.X)=0.X by BCIALG_1:1;
  then (y\0.X)\(y\x)\(x\0.X) in I by BCIALG_1:def 18;
  then y\(y\x)\(x\0.X) in I by BCIALG_1:2;
  hence y\(y\x)\x in I by BCIALG_1:2;
  (y\0.X)\(y\x)\(x\0.X)=0.X by BCIALG_1:1;
  then (y\0.X)\(y\x)<=(x\0.X) by BCIALG_1:def 11;
  then (y\0.X)\(y\x)\(x\y)<=(x\0.X)\(x\y) by BCIALG_1:5;
  then y\(y\x)\(x\y)<=(x\0.X)\(x\y) by BCIALG_1:2;
  then y\(y\x)\(x\y)<=x\(x\y) by BCIALG_1:2;
  then y\(y\x)\(x\y)\(x\(x\y)) =0.X by BCIALG_1:def 11;
  then y\(y\x)\(x\y)\(x\(x\y)) in I by BCIALG_1:def 18;
  hence thesis by A1,BCIALG_1:def 18;
end;

theorem
  {0.X} is commutative Ideal of X iff for x,y being Element of X holds x
  \(x\y) <= y\(y\x)
proof
  thus {0.X} is commutative Ideal of X implies for x,y being Element of X
  holds x\(x\y) <= y\(y\x)
  proof
    assume {0.X} is commutative Ideal of X;
    then X is commutative BCK-algebra by Th36;
    hence thesis by BCIALG_3:1;
  end;
  assume for x,y being Element of X holds x\(x\y) <= y\(y\x);
  then X is commutative BCK-algebra by BCIALG_3:1;
  hence thesis by Th36;
end;

theorem
  {0.X} is commutative Ideal of X iff for x,y being Element of X holds x
  \y = x\(y\(y\x))
proof
  thus {0.X} is commutative Ideal of X implies for x,y being Element of X
  holds x\y = x\(y\(y\x))
  proof
    assume {0.X} is commutative Ideal of X;
    then X is commutative BCK-algebra by Th36;
    hence thesis by BCIALG_3:3;
  end;
  assume for x,y being Element of X holds x\y = x\(y\(y\x));
  then X is commutative BCK-algebra by BCIALG_3:3;
  hence thesis by Th36;
end;

theorem
  {0.X} is commutative Ideal of X iff for x,y being Element of X holds x
  \(x\y) = y\(y\(x\(x\y)))
proof
  thus {0.X} is commutative Ideal of X implies for x,y being Element of X
  holds x\(x\y) = y\(y\(x\(x\y)))
  proof
    assume {0.X} is commutative Ideal of X;
    then X is commutative BCK-algebra by Th36;
    hence thesis by BCIALG_3:4;
  end;
  assume for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y)));
  then X is commutative BCK-algebra by BCIALG_3:4;
  hence thesis by Th36;
end;

theorem
  {0.X} is commutative Ideal of X iff for x,y being Element of X st x<=
  y holds x= y\(y\x)
proof
  thus {0.X} is commutative Ideal of X implies for x,y being Element of X st x
  <= y holds x= y\(y\x)
  proof
    assume {0.X} is commutative Ideal of X;
    then X is commutative BCK-algebra by Th36;
    hence thesis by BCIALG_3:5;
  end;
  assume for x,y being Element of X st x<= y holds x= y\(y\x);
  then X is commutative BCK-algebra by BCIALG_3:5;
  hence thesis by Th36;
end;

theorem
  {0.X} is commutative Ideal of X implies (for x,y being Element of X
holds (x\y=x iff y\(y\x)=0.X)) & (for x,y being Element of X st x\y=x holds y\x
=y) & (for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x) &(for x,
  y being Element of X holds x\(y\(y\x))=x\y & (x\y)\((x\y)\x)=x\y) & for x,y,a
  being Element of X st x <= a holds (a\y)\((a\y)\(a\x)) = (a\y)\(x\y)
proof
  assume {0.X} is commutative Ideal of X;
  then
A1: X is commutative BCK-algebra by Th36;
  hence for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X) by BCIALG_3:9;
  thus for x,y being Element of X st x\y=x holds y\x=y by A1,BCIALG_3:7;
  thus for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x by A1,
BCIALG_3:8;
  thus for x,y being Element of X holds x\(y\(y\x))=x\y &(x\y)\((x\y)\x)=x\y
  by A1,BCIALG_3:10;
  thus thesis by A1,BCIALG_3:11;
end;

theorem
  (for I being Ideal of X holds I is commutative Ideal of X) iff for x,y
  being Element of X holds x\(x\y) <= y\(y\x)
proof
  thus (for I being Ideal of X holds I is commutative Ideal of X) implies for
  x,y being Element of X holds x\(x\y) <= y\(y\x)
  proof
    assume for I being Ideal of X holds I is commutative Ideal of X;
    then X is commutative BCK-algebra by Th37;
    hence thesis by BCIALG_3:1;
  end;
  assume for x,y being Element of X holds x\(x\y) <= y\(y\x);
  then X is commutative BCK-algebra by BCIALG_3:1;
  hence thesis by Th37;
end;

theorem
  (for I being Ideal of X holds I is commutative Ideal of X) iff for x,y
  being Element of X holds x\y = x\(y\(y\x))
proof
  thus (for I being Ideal of X holds I is commutative Ideal of X) implies for
  x,y being Element of X holds x\y = x\(y\(y\x))
  proof
    assume for I being Ideal of X holds I is commutative Ideal of X;
    then X is commutative BCK-algebra by Th37;
    hence thesis by BCIALG_3:3;
  end;
  assume for x,y being Element of X holds x\y = x\(y\(y\x));
  then X is commutative BCK-algebra by BCIALG_3:3;
  hence thesis by Th37;
end;

theorem
  (for I being Ideal of X holds I is commutative Ideal of X) iff for x,y
  being Element of X holds x\(x\y) = y\(y\(x\(x\y)))
proof
  thus (for I being Ideal of X holds I is commutative Ideal of X) implies for
  x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y)))
  proof
    assume for I being Ideal of X holds I is commutative Ideal of X;
    then X is commutative BCK-algebra by Th37;
    hence thesis by BCIALG_3:4;
  end;
  assume for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y)));
  then X is commutative BCK-algebra by BCIALG_3:4;
  hence thesis by Th37;
end;

theorem
  (for I being Ideal of X holds I is commutative Ideal of X) iff for x,y
  being Element of X st x<= y holds x= y\(y\x)
proof
  thus (for I being Ideal of X holds I is commutative Ideal of X) implies for
  x,y being Element of X st x<= y holds x= y\(y\x)
  proof
    assume for I being Ideal of X holds I is commutative Ideal of X;
    then X is commutative BCK-algebra by Th37;
    hence thesis by BCIALG_3:5;
  end;
  assume for x,y being Element of X st x<= y holds x= y\(y\x);
  then X is commutative BCK-algebra by BCIALG_3:5;
  hence thesis by Th37;
end;

theorem
  (for I being Ideal of X holds I is commutative Ideal of X) implies (
  for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X)) & (for x,y being
  Element of X st x\y=x holds y\x=y) & (for x,y,a being Element of X st y <= a
holds (a\x)\(a\y) = y\x) &(for x,y being Element of X holds x\(y\(y\x))=x\y & (
x\y)\((x\y)\x)=x\y) & for x,y,a being Element of X st x <= a holds (a\y)\((a\y)
  \(a\x)) = (a\y)\(x\y)
proof
  assume for I being Ideal of X holds I is commutative Ideal of X;
  then
A1: X is commutative BCK-algebra by Th37;
  hence for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X) by BCIALG_3:9;
  thus for x,y being Element of X st x\y=x holds y\x=y by A1,BCIALG_3:7;
  thus for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x by A1,
BCIALG_3:8;
  thus for x,y being Element of X holds x\(y\(y\x))=x\y &(x\y)\((x\y)\x)=x\y
  by A1,BCIALG_3:10;
  thus thesis by A1,BCIALG_3:11;
end;

begin :: implicative Ideal of X & positive-implicative-ideal

definition
  let X be BCK-algebra;
  mode implicative-ideal of X -> non empty Subset of X means
    :Def7:
    0.X in it
    & for x,y,z being Element of X st (x\(y\x))\z in it& z in it holds x in it;
  existence
  proof
    take X1=the carrier of X;
    X1 c= the carrier of X;
    hence thesis;
  end;
end;

reserve X for BCK-algebra;
reserve I for Ideal of X;

theorem Th50:
  I is implicative-ideal of X iff for x,y being Element of X st x\
  (y\x) in I holds x in I
proof
A1: (for x,y being Element of X st x\(y\x) in I holds x in I) implies I is
  implicative-ideal of X
  proof
    assume
A2: for x,y being Element of X st x\(y\x) in I holds x in I;
A3: for x,y,z being Element of X st (x\(y\x))\z in I & z in I holds x in I
    proof
      let x,y,z be Element of X;
      assume (x\(y\x))\z in I & z in I;
      then x\(y\x) in I by BCIALG_1:def 18;
      hence thesis by A2;
    end;
    0.X in I by BCIALG_1:def 18;
    hence thesis by A3,Def7;
  end;
  I is implicative-ideal of X implies for x,y being Element of X st x\(y\x
  ) in I holds x in I
  proof
    assume
A4: I is implicative-ideal of X;
    let x,y be Element of X;
    assume x\(y\x) in I;
    then
A5: x\(y\x)\0.X in I by BCIALG_1:2;
    thus thesis by A4,A5,Def7;
  end;
  hence thesis by A1;
end;

definition
  let X be BCK-algebra;
  mode positive-implicative-ideal of X -> non empty Subset of X means
    :Def8:
0.X in it &for x,y,z being Element of X st (x\y)\z in it & y\z in it holds x\z
    in it;
  existence
  proof
    take X1=the carrier of X;
    X1 c= the carrier of X;
    hence thesis;
  end;
end;

theorem Th51:
  I is positive-implicative-ideal of X iff for x,y being Element
  of X st (x\y)\y in I holds x\y in I
proof
  thus I is positive-implicative-ideal of X implies for x,y being Element of X
  st (x\y)\y in I holds x\y in I
  proof
    assume
A1: I is positive-implicative-ideal of X;
    let x,y be Element of X;
    y\y =0.X by BCIALG_1:def 5;
    then
A2: y\y in I by A1,Def8;
    assume (x\y)\y in I;
    hence thesis by A1,A2,Def8;
  end;
  thus (for x,y being Element of X st (x\y)\y in I holds x\y in I) implies I
  is positive-implicative-ideal of X
  proof
    assume
A3: for x,y being Element of X st (x\y)\y in I holds x\y in I;
A4: for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x\z in I
    proof
      let x,y,z be Element of X;
      assume that
A5:   (x\y)\z in I and
A6:   y\z in I;
      ((x\z)\z)\((x\y)\z)\((x\z)\(x\y))=0.X by BCIALG_1:def 3;
      then ((x\z)\z)\((x\y)\z)<=(x\z)\(x\y) by BCIALG_1:def 11;
      then ((x\z)\z)\((x\y)\z)\(y\z)<=(x\z)\(x\y)\(y\z) by BCIALG_1:5;
      then ((x\z)\z)\((x\y)\z)\(y\z)<=0.X by BCIALG_1:1;
      then ((x\z)\z)\((x\y)\z)\(y\z)\0.X=0.X by BCIALG_1:def 11;
      then ((x\z)\z)\((x\y)\z)\(y\z)=0.X by BCIALG_1:2;
      then ((x\z)\z)\((x\y)\z)<=y\z by BCIALG_1:def 11;
      then ((x\z)\z)\((x\y)\z) in I by A6,Th5;
      then (x\z)\z in I by A5,BCIALG_1:def 18;
      hence thesis by A3;
    end;
    0.X in I by BCIALG_1:def 18;
    hence thesis by A4,Def8;
  end;
end;

theorem Th52:
  (for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x
\z in I) implies for x,y,z being Element of X st (x\y)\z in I holds (x\z)\(y\z)
  in I
proof
  assume
A1: for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x\z in I;
  let x,y,z be Element of X;
  x\(y\z) \ (x\y) \ (y\(y\z)) =0.X by BCIALG_1:1;
  then x\(y\z) \ (x\y)<=y\(y\z) by BCIALG_1:def 11;
  then
A2: x\(y\z) \ (x\y)\z<=y\(y\z)\z by BCIALG_1:5;
  y\(y\z)\z =y\z\(y\z) by BCIALG_1:7;
  then x\(y\z) \ (x\y)\z<=0.X by A2,BCIALG_1:def 5;
  then x\(y\z) \ (x\y)\z\0.X=0.X by BCIALG_1:def 11;
  then x\(y\z) \ (x\y)\z=0.X by BCIALG_1:2;
  then
A3: (x\(y\z))\(x\y)\z in I by BCIALG_1:def 18;
  assume (x\y)\z in I;
  then x\(y\z)\z in I by A1,A3;
  hence thesis by BCIALG_1:7;
end;

theorem Th53:
  (for x,y,z being Element of X st (x\y)\z in I holds (x\z)\(y\z)
  in I) implies I is positive-implicative-ideal of X
proof
  assume
A1: for x,y,z being Element of X st (x\y)\z in I holds (x\z)\(y\z) in I;
A2: for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x\z in I
  proof
    let x,y,z be Element of X;
    assume that
A3: (x\y)\z in I and
A4: y\z in I;
    (x\z)\(y\z) in I by A1,A3;
    hence thesis by A4,BCIALG_1:def 18;
  end;
  0.X in I by BCIALG_1:def 18;
  hence thesis by A2,Def8;
end;

theorem
  I is positive-implicative-ideal of X iff for x,y,z being Element of X
  st (x\y)\z in I & y\z in I holds x\z in I
proof
A1: 0.X in I by BCIALG_1:def 18;
  thus I is positive-implicative-ideal of X implies for x,y,z being Element of
  X st (x\y)\z in I & y\z in I holds x\z in I by Def8;
  assume
  for x,y,z being Element of X st (x\y)\z in I & y\z in I holds x\z in I;
  hence thesis by A1,Def8;
end;

theorem
  I is positive-implicative-ideal of X iff for x,y,z being Element of X
  st (x\y)\z in I holds (x\z)\(y\z) in I
proof
  I is positive-implicative-ideal of X implies for x,y,z being Element of
  X st (x\y)\z in I & y\z in I holds x\z in I by Def8;
  hence thesis by Th52,Th53;
end;

theorem
  for I,A being Ideal of X st I c= A & I is positive-implicative-ideal
  of X holds A is positive-implicative-ideal of X
proof
  let I,A be Ideal of X;
  assume that
A1: I c= A and
A2: I is positive-implicative-ideal of X;
  for x,y being Element of X st (x\y)\y in A holds x\y in A
  proof
    let x,y be Element of X;
    (x\((x\y)\y)\y) \y = ((x\y)\((x\y)\y))\y by BCIALG_1:7
      .=(x\y\y)\ ((x\y)\y) by BCIALG_1:7
      .=0.X by BCIALG_1:def 5;
    then (x\((x\y)\y)\y) \y in I by BCIALG_1:def 18;
    then (x\((x\y)\y)\y) in I by A2,Th51;
    then
A3: (x\y)\((x\y)\y) in I by BCIALG_1:7;
    assume (x\y)\y in A;
    hence thesis by A1,A3,BCIALG_1:def 18;
  end;
  hence thesis by Th51;
end;

theorem
  I is implicative-ideal of X implies I is commutative Ideal of X & I is
  positive-implicative-ideal of X
proof
  assume
A1: I is implicative-ideal of X;
A2: for x,y being Element of X st x\y in I holds x\(y\(y\x)) in I
  proof
    let x,y be Element of X;
    (x\(y\(y\x)))\x = (x\x)\(y\(y\x)) by BCIALG_1:7
      .=(y\(y\x))` by BCIALG_1:def 5
      .=0.X by BCIALG_1:def 8;
    then (x\(y\(y\x)))<=x by BCIALG_1:def 11;
    then y\x<=y\(x\(y\(y\x))) by BCIALG_1:5;
    then (x\(y\(y\x)))\(y\(x\(y\(y\x))))<=(x\(y\(y\x)))\(y\x) by BCIALG_1:5;
    then
A3: (x\(y\(y\x)))\(y\(x\(y\(y\x))))\(x\y) <=(x\(y\(y\x)))\(y\x)\(x\y) by
BCIALG_1:5;
    (x\(y\(y\x)))\(y\x)=(x\(y\x))\(y\(y\x)) by BCIALG_1:7;
    then (x\(y\(y\x)))\(y\(x\(y\(y\x))))\(x\y)<=0.X by A3,BCIALG_1:def 3;
    then (x\(y\(y\x)))\(y\(x\(y\(y\x))))\(x\y)\0.X=0.X by BCIALG_1:def 11;
    then (x\(y\(y\x)))\(y\(x\(y\(y\x))))\(x\y)=0.X by BCIALG_1:2;
    then
A4: (x\(y\(y\x)))\(y\(x\(y\(y\x))))<=x\y by BCIALG_1:def 11;
    assume x\y in I;
    hence thesis by A1,A4,Th5,Th50;
  end;
  for x,y being Element of X st (x\y)\y in I holds x\y in I
  proof
    let x,y be Element of X;
    (x\y)\(x\(x\y))\((x\y)\y)=0.X by BCIALG_1:1;
    then
A5: (x\y)\(x\(x\y))<=((x\y)\y) by BCIALG_1:def 11;
    assume (x\y)\y in I;
    hence thesis by A1,A5,Th5,Th50;
  end;
  hence thesis by A2,Th33,Th51;
end;