:: Ideals of BCI-Algebras and Their Properties
::  by Chenglong Wu and Yuzhong Ding
:: 
:: Received March 3, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies BINOP_1, BCIALG_1, BOOLE, RLVECT_1, WAYBEL15, FILTER_2, PRE_TOPC,
      SUBSET_1, BCIIDEAL, ASYMPT_0, CHORD;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, NUMBERS, FUNCT_1, RLVECT_1,
      BINOP_1, STRUCT_0, GROUP_1, VECTSP_1, MIDSP_1, VECTSP_2, NAT_1, RELAT_1,
      BCIALG_1, BCIALG_2, BCIALG_3;
 constructors TARSKI, BINOP_1, REAL_1, BINOP_2, RLVECT_1, MEMBERED, XBOOLE_0,
      GROUP_1, VECTSP_1, MIDSP_1, FUNCT_1, VECTSP_2, REALSET1, STRUCT_0,
      SUBSET_1, ENUMSET1, ZFMISC_1, RELAT_1, BCIALG_1, POWER, BCIALG_2,
      BCIALG_3;
 registrations STRUCT_0, RLVECT_1, RELSET_1, MEMBERED, GROUP_1, XBOOLE_0,
      REALSET1, SUBSET_1, RELAT_1, BCIALG_1, BCIALG_2, BCIALG_3;
 requirements NUMERALS, SUBSET, ARITHM, BOOLE;
 definitions BCIALG_1, TARSKI, XBOOLE_0;
 theorems BCIALG_1, TARSKI, XBOOLE_0, BCIALG_2, BCIALG_3;

begin :: Ideal of X

 reserve X,Y for BCI-algebra;
 reserve X1 for non empty Subset of X;
 reserve A,I,I1 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 A2:((x\(y\z))\(x\(y\u)))\(z\u)<=((y\u)\(y\z))\(z\u) by BCIALG_1:5;
A3:((y\u)\(y\z))\(z\u)=((y\u)\(z\u))\(y\z) by BCIALG_1:7;
((x\(y\z))\(x\(y\u)))\(z\u)<=0.X by A2,A3,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 A2:(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;
A3:((y\(z\v))\(y\(z\u)))\((z\u)\(z\v))=((y\(z\v))\((z\u)\(z\v)))\(y\(z\u))
                                                            by BCIALG_1:7;
 (x\(y\(z\u)))\(x\(y\(z\v)))\((z\u)\(z\v))<=0.X by A2,A3,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 B1:(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 BCIALG_1:def 11,B1;
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;
A1:(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);
A5:((0.X\x)\(0.X\y))\(y\x)=((0.X\x)\(y\x))\(0.X\y) by BCIALG_1:7;
 ((0.X\x)\(0.X\y))\(y\x)=(((y\x)`)\x)\(0.X\y) by A5,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;
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 P141:  ::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 A0:x is Element of B;
A1:x in B by A0;
  x in {x1 where x1 is Element of X:x1 is minimal};
  then consider x1 being Element of X such that
B1:x=x1&x1 is minimal;
  consider x3 being Element of X such that
C1:x=x3&b<=x3 by A1;
  b\x=0.X by BCIALG_1:def 11, C1;
  hence thesis by BCIALG_1:def 14,B1;
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 A0:x is Element of B;
 A1:x in B by A0;
 x in {x1 where x1 is Element of X:x1 is minimal};
       then consider x1 being Element of X such that
        B1:x=x1&x1 is minimal;
      consider x3 being Element of X such that
        C1:x=x3&b<=x3 by A1;
       b\x=0.X by BCIALG_1:def 11, C1;
        hence thesis by BCIALG_1:def 14,B1;
end;

theorem
   initial_section(a) c= A
proof
   let b be set;
   assume b in initial_section(a);
   then consider x1 being Element of X such that
A3:b=x1 & x1<=a;
   thus b in A by A3,P141;
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);
 assume A0:P is Ideal of X;
Lm1:x in {0.X} iff x in B/\P
  proof
   thus x in {0.X} implies x in B/\P
   proof
   A1:0.X in B by BCIALG_1:19;
   0.X in P;
  then 0.X in B/\P by A1,XBOOLE_0:def 3;
  hence thesis by TARSKI:def 1;
   end;
   thus x in B/\P implies x in {0.X}
   proof
   assume A1: x in B/\P;
   then A2:x in B by XBOOLE_0:def 3;
        consider x1 being Element of X such that
        B1:x=x1&0.X<=x1 by A2;
     C: x in {x2 where x2 is Element of X:x2 is minimal} by A1,XBOOLE_0:def 3;
       consider x2 being Element of X such that
        B2:x=x2&x2 is minimal by C;
    0.X\x=0.X by BCIALG_1:def 11,B1;
    then 0.X=x by B2,BCIALG_1:def 14;
   hence thesis by TARSKI:def 1;
   end;
  end;
 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 A1: x\a in P;
        x in P by A0,BCIALG_1:def 18,A1;
       then x in B /\ P by XBOOLE_0:def 3;
       then x in {0.X} by Lm1;
       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);
  assume C1:P is Ideal of X;
  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;
  hence thesis by C1,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 B1:A/\I={0.X};
        let x be Element of A;
        let y be Element of I;
        C:(x\y)\x = x\x\y by BCIALG_1:7
        .=y` by BCIALG_1:def 5
        .=0.X by BCIALG_1:def 8;
        C1:(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;
         (x\(x\y))<=x by BCIALG_1:def 11,C1;
        then A1:x\(x\y) in A by P141;
          x\(x\y)\y=0.X by BCIALG_1:1;
         then x\(x\y)<=y by BCIALG_1:def 11;
         then x\(x\y) in I by P141;
                    then x\(x\y) in {0.X} by B1,A1,XBOOLE_0:def 3;
          then x\(x\y)=0.X by TARSKI:def 1;
                  hence thesis by C,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 A1: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 C:x in A/\I;
          then reconsider xxx=x as Element of A by XBOOLE_0:def 3;
            reconsider xx=x as Element of I by C,XBOOLE_0:def 3;
           xxx\xx=xxx by A1;
          then x=0.X by BCIALG_1:def 5;
        hence thesis by TARSKI:def 1;
         end;
        let x be set;
         assume A0:x in {0.X};
          A2:x =0.X by A0,TARSKI:def 1;
         A3:0.X in A by BCIALG_1:def 18;
         0.X in I by BCIALG_1:def 18;
         hence thesis by A2,A3,XBOOLE_0:def 3;
        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 A0:X is quasi-associative;
   for x being Element of A holds x` in A
   proof
   let x be Element of A;
   x`<=x by BCIALG_1:71,A0;
   hence thesis by P141;
   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 :Defzzz:
    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 Ideal of X;
  existence
  proof
    take Y={0.X};
    reconsider YY=Y as Ideal of X by BCIALG_1:43;
    A1: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;
A3: 0.X in YY&for x,y,z being Element of X st x\(y\z) in YY&y\z in YY
              holds x=0.X by A1,TARSKI:def 1;
    0.X in YY&for x,y,z being Element of X st x\(y\z) in YY&y\z in YY
              holds x in YY by A3;
    hence thesis by Defzzz;
  end;
end;

definition let X be BCI-algebra;
  mode associative-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 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;
   then A3:0.X in X1 by Def8;
   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,Def8;
   end;
   hence thesis by BCIALG_1:def 18,A3;
end;

theorem TL31321:
  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 A:I is associative-ideal of X;
      let x,y,z such that A1:(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 A5:(x\(x\y)\(y\z))\z <= (y\(y\z))\z by BCIALG_1:5;
       C:(y\(y\z))\z =0.X by BCIALG_1:1;
       ((x\(x\y)\(y\z))\z)\0.X=0.X by BCIALG_1:def 11,A5,C;
      then ((x\(x\y))\(y\z))\z =0.X by BCIALG_1:2;
      then A8:((x\(x\y))\(y\z))\z in I by Def8,A;
       ((x\(y\z))\(x\y))\z in I by A8, BCIALG_1:7;
      hence x\(y\z) in I by Def8,A1,A;
    end;
      assume B:for x,y,z st (x\y)\z in I holds x\(y\z) in I;
      B1:0.X in I by BCIALG_1:def 18;
      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 C:(x\y)\z in I & y\z in I;
           x\(y\z) in I by B,C;
          hence x in I by C,BCIALG_1:def 18;
        end;
      hence I is associative-ideal of X by B1,Def8;
end;

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

theorem
  (for x being Element of X holds x\(0.X\x) in I) implies
                             I is closed Ideal of X
proof
  assume B: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;
    C3:(0.X\x1)\x1=(0.X\(0.X\(0.X\x1)))\x1 by BCIALG_1:8;
    (0.X\x1)\x1=(0.X\x1)\(0.X\(0.X\x1)) by C3,BCIALG_1:7;
    then (0.X\x1)\x1 in I by B;
    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 :Def1:
    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;
  A3:0.X in X1 by Def1,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;
    assume x\y in X1 & y in X1;
    then (x\0.X)\y in X1 & y in X1 by BCIALG_1:2;
    then (x\0.X)\(y\0.X) in X1 & y in X1 by BCIALG_1:2;
    hence thesis by A1,Def1;
  end;
  hence thesis by A3,BCIALG_1:def 18;
end;

theorem TL352:
  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;
  then BB:0.X in I by Def1;
  let x be set;
  assume x in BCK-part(X);
  then consider x1 being Element of X such that
  B1:x=x1&0.X<=x1;
  reconsider x as Element of X by B1;
       0.X\x = 0.X by BCIALG_1:def 11,B1;
  then 0.X\(0.X\x)=0.X by BCIALG_1:2;
  then (x\x)\(0.X\x)=0.X by BCIALG_1:def 5;
  hence thesis by Def1,A1,BB;
end;

theorem
   BCK-part(X) is p-ideal of X
proof
     set A = BCK-part(X);
     0.X in A & for x,y,z being Element of X st
        (x\z)\(y\z) in A & y in A holds x in A
  proof
 C1:now let x,y,z be Element of X;
    assume B1: (x\z)\(y\z) in A & y in A;
    then consider d being Element of X such that
    B4:y=d & 0.X<=d;
     B5:y` = 0.X by B4,BCIALG_1:def 11;
    consider c being Element of X such that
    B3:((x\z)\(y\z) = c&0.X<=c) by B1;
         ((x\z)\(y\z))`= 0.X by BCIALG_1:def 11,B3;
         then ((x\z)`)\((y\z)`)=0.X by BCIALG_1:9;
         then (x`\z`)\((y\z)`)=0.X by BCIALG_1:9;
         then ((x`\z`)\(0.X\z`))\(x`\0.X)=(x`\0.X)` by B5,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;
   hence thesis by C1;
  end;
  hence thesis by Def1;
end;

theorem TL358:
  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 A:I is p-ideal of X;
      let x,y such that A2: x in I & x <= y;
      AC:BCK-part(X) c= I by A,TL352;
      A3:x\y = 0.X & x in I by BCIALG_1:def 11,A2;
      then (y\x)`=x\y by BCIALG_1:6;
      then 0.X <= y\x by BCIALG_1:def 11,A3;
      then y\x in BCK-part(X);
      hence thesis by A2,BCIALG_1:def 18,AC;
    end;
      assume B:for x,y st x in I & x<=y holds y in I;
       B1:0.X in I by BCIALG_1:def 18;
      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 C1:(x\z)\(y\z) in I & 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 C1,B;
         hence x in I by C1,BCIALG_1:def 18;
        end;
   hence I is p-ideal of X by Def1,B1;
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 A: 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 A2,TL358,A;
    end;
      assume B:for x,y,z st (x\z)\(y\z) in I holds x\y in I;
       B1:0.X in I by BCIALG_1:def 18;
      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 C1:(x\z)\(y\z) in I&y in I;
           x\y in I by B,C1;
          hence x in I by BCIALG_1:def 18,C1;
        end;
      hence I is p-ideal of X by B1,Def1;
end;

begin :: P132: commutative Ideal of X

definition let X be BCK-algebra, IT be Ideal of X;
  attr IT is commutative means :Def4:
    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 Ideal of X;
existence
   proof
    set X1 = BCK-part(X);
    take X1;
 A2:X1 is Ideal of X
 proof
A1: 0.X in BCK-part(X) by BCIALG_1:19;
     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
        B1:x\y=x1&0.X<=x1 by A2;
        consider x2 being Element of X such that
        B2:y=x2&0.X<=x2 by A2;
          A6:y`=0.X by B2,BCIALG_1:def 11;
        (x\y)`=0.X by B1,BCIALG_1:def 11;
     then x`\0.X = 0.X by A6,BCIALG_1:9;
     then 0.X\x=0.X by BCIALG_1:2;
     then 0.X<= x by BCIALG_1:def 11;
     hence x in X1;
    end;
    hence thesis by BCIALG_1:def 18,A1;
 end;
 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;
     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;
    hence thesis by A2,Def4;
   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);
 A2:B is Ideal of X
 proof
A1: 0.X in BCK-part(X) by BCIALG_1:19;
 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 & y in B;
 consider x1 being Element of X such that
 B1:x\y=x1&0.X<=x1 by A2;
 consider x2 being Element of X such that
 B2:y=x2&0.X<=x2 by A2;
  A7:(x\y)`=0.X by B1,BCIALG_1:def 11;
     x`\y`=0.X by A7,BCIALG_1:9;
 then x`\0.X = 0.X by B2,BCIALG_1:def 11;
 then 0.X\x=0.X by BCIALG_1:2;
 then 0.X<= x by BCIALG_1:def 11;
 hence x in B;
    end;
    hence thesis by BCIALG_1:def 18,A1;
 end;
  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 (x\y)\z in B & 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;
    hence thesis by A2,Def4;
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;
  assume C:X is p-Semisimple BCI-algebra;
  set X1={0.X};
     A:{0.X} is Ideal of X
    proof
      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 xx in the carrier of X;
     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 BCIALG_1:2;
      hence thesis by TARSKI:def 1;
      end;
     hence thesis by A1,A2,BCIALG_1:def 18;
    end;
    reconsider X1 as Ideal of X by A;
     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 CC:(x\y)\z in X1& z in X1;
      B3:y is atom by C,BCIALG_1:52;
     (x\y)\z=0.X & z=0.X by CC,TARSKI:def 1;
    then x\y = 0.X by BCIALG_1:2;
    then x=y by BCIALG_1:def 14,B3;
    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 Def4;
  end;

Lm3: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 A1:x in the carrier of X;
  consider x1 being Element of X such that
A2:x=x1 by A1;
  x1` = 0.X by BCIALG_1:def 8;
  then 0.X <= x1 by BCIALG_1:def 11;
  hence x in BCK-part(X) by A2;
end;

 reserve X for BCK-algebra;

theorem P25010:
  BCK-part(X) = the carrier of X
proof
  the carrier of X c= BCK-part(X) by Lm3;
  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 P25010;
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 P25010;
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 P25010;
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 P25010;
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 P25010;
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 P25010;
end;

 reserve X for BCK-algebra;

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);
 B0: the carrier of X=B by P25010;
 A2:B is Ideal of X
 proof
A1: 0.X in BCK-part(X) by BCIALG_1:19;
 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 & y in B;
  consider x1 being Element of X such that
 B1:x\y=x1&0.X<=x1 by A2;
 consider x2 being Element of X such that
 B2:y=x2&0.X<=x2 by A2;
 A7:(x\y)`=0.X by B1,BCIALG_1:def 11;
    x`\y`=0.X by A7,BCIALG_1:9;
 then x`\0.X = 0.X by B2,BCIALG_1:def 11;
 then 0.X\x=0.X by BCIALG_1:2;
     then 0.X<= x by BCIALG_1:def 11;
     hence x in B;
 end;
    hence thesis by BCIALG_1:def 18,A1;
 end;
  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 (x\y)\z in B & 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;
    hence thesis by A2,Def4,B0;
   end;

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

theorem TL251:
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
assume A1:I is commutative Ideal of X;
let x,y be Element of X such that A2:x\y in I;
 A3:(x\y)\0.X in I by A2, BCIALG_1:2;
0.X in I by BCIALG_1:def 18;
hence thesis by A1,A3,Def4;
end;
assume A: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 such that A2:(x\y)\z in I & z in I;
     x\y in I by A2,BCIALG_1:def 18;
     hence thesis by A;
    end;
hence thesis by Def4;
end;

theorem TL252:
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 A1:I c= A & 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;
        assume A2:x\y in A;
         (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 TL251,A1;
        then (x\(x\y))\(y\(y\(x\(x\y)))) in A by A1;
        then (x\(y\(y\(x\(x\y)))))\(x\y) in A by BCIALG_1:7;
        then A5:(x\(y\(y\(x\(x\y))))) in A by A2,BCIALG_1:def 18;
        (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 A6:x\(x\y)<=x by BCIALG_1:def 11;
        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;
        then y\(y\(x\(x\y)))<=y\(y\x) by A6;
        then x\(y\(y\x))<=x\(y\(y\(x\(x\y)))) by BCIALG_1:5;
        hence thesis by P141,A5;
        end;
hence thesis by TL251;
end;

theorem TL253:
(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 x in I by BCIALG_1:def 18;
end;
hence thesis by A1,TL252;
end;
end;

theorem TL254:
{0.X} is commutative Ideal of X iff
X is commutative BCK-algebra
proof
thus {0.X} is commutative Ideal of X implies
X is commutative BCK-algebra
proof
assume A:{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 B2:x\y=0.X by BCIALG_1:def 11;
 B4:(y\(y\x))\x=0.X by BCIALG_1:1;
x\y in {0.X} by B2,TARSKI:def 1;
then x\(y\(y\x)) in {0.X} by A,TL251;
then x\(y\(y\x))=0.X by TARSKI:def 1;
hence thesis by B4,BCIALG_1:def 7;
 end;
 hence thesis by BCIALG_3:5;
end;
assume A:X is commutative BCK-algebra;
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;
  for x,y being Element of X st x\y in {0.X} holds x\(y\(y\x)) in {0.X}
    by A,A1;
  hence thesis by TL251,BCIALG_1:43;
end;

theorem TL255:
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 A:X is commutative BCK-algebra;
 {0.X} is commutative Ideal of X by TL254,A;
 hence thesis by TL253;
end;
assume A:(for I being Ideal of X holds I is commutative Ideal of X);
{0.X} is commutative Ideal of X by TL253,A;
hence thesis by TL254;
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 TL254;
hence thesis by TL255;
end;
assume for I being Ideal of X holds I is commutative Ideal of X;
then X is commutative BCK-algebra by TL255;
hence thesis by TL254;
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 B1: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 B1;
    (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 B1,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 A:{0.X} is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL254;
    hence thesis by BCIALG_3:1;
  end;
 assume A:(for x,y being Element of X holds x\(x\y) <= y\(y\x));
    X is commutative BCK-algebra by A,BCIALG_3:1;
    hence thesis by TL254;
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 A:{0.X} is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL254;
    hence thesis by BCIALG_3:3;
  end;
 assume A:(for x,y being Element of X holds x\y = x\(y\(y\x)) );
    X is commutative BCK-algebra by A,BCIALG_3:3;
    hence thesis by TL254;
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 A:{0.X} is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL254;
    hence thesis by BCIALG_3:4;
  end;
  assume A:(for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y))) );
  X is commutative BCK-algebra by A,BCIALG_3:4;
  hence thesis by TL254;
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 A:{0.X} is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL254;
    hence thesis by BCIALG_3:5;
  end;
  assume A:(for x,y being Element of X st x<= y holds x= y\(y\x));
  X is commutative BCK-algebra by A,BCIALG_3:5;
  hence thesis by TL254;
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 A:{0.X} is commutative Ideal of X;
A1:X is commutative BCK-algebra by A,TL254;
thus (for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X))
                                                              by A1,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 (for x,y,a being Element of X
    st x <= a holds (a\y)\((a\y)\(a\x)) = (a\y)\(x\y)) 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 A:(for I being Ideal of X holds I is commutative Ideal of X);
    X is commutative BCK-algebra by A,TL255;
    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 TL255;
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 A:for I being Ideal of X holds I is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL255;
    hence thesis by BCIALG_3:3;
  end;
 assume A:for x,y being Element of X holds x\y = x\(y\(y\x));
    X is commutative BCK-algebra by A,BCIALG_3:3;
    hence thesis by TL255;
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 A:(for I being Ideal of X holds I is commutative Ideal of X);
    X is commutative BCK-algebra by A,TL255;
    hence thesis by BCIALG_3:4;
  end;
 assume A:(for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y))) );
   X is commutative BCK-algebra by A,BCIALG_3:4;
    hence thesis by TL255;
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 A:for I being Ideal of X holds I is commutative Ideal of X;
    X is commutative BCK-algebra by A,TL255;
    hence thesis by BCIALG_3:5;
  end;
 assume A:for x,y being Element of X st x<= y holds x= y\(y\x);
 X is commutative BCK-algebra by A,BCIALG_3:5;
 hence thesis by TL255;
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 A:(for I being Ideal of X holds I is commutative Ideal of X);
A1:X is commutative BCK-algebra by A,TL255;
thus (for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X))
                                                              by A1,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 (for x,y,a being Element of X
    st x <= a holds (a\y)\((a\y)\(a\x)) = (a\y)\(x\y)) 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 :Def2:
    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,A for Ideal of X;
 reserve x,y,z for Element of X;

theorem P351:
 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
C1:  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 A:I is implicative-ideal of X;
let x,y be Element of X;
assume x\(y\x) in I;
then A2:x\(y\x)\0.X in I by BCIALG_1:2;
0.X in I by A,Def2;
hence thesis by A,A2,Def2;
end;
  (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 B:for x,y being Element of X st x\(y\x) in I holds x in I;
D: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 B;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by Def2,D;
end;
hence thesis by C1;
end;

definition let X be BCK-algebra;
  mode positive-implicative-ideal of X -> non empty Subset of X means :Def5:
    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 TL341:
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 A:I is positive-implicative-ideal of X;
let x,y be Element of X;
assume B1:(x\y)\y in I;
y\y =0.X by BCIALG_1:def 5;
then y\y in I by A,Def5;
hence thesis by Def5,B1,A;
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 A:for x,y being Element of X st (x\y)\y in I holds x\y in I;
 A1:0.X in I by BCIALG_1:def 18;
 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 B1:(x\y)\z in I & 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 P141,B1;
then (x\z)\z in I by BCIALG_1:def 18,B1;
hence thesis by A;
end;
hence thesis by A1,Def5;
 end;
end;

theorem TL3421:
(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 A: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;
assume A1:(x\y)\z in I;
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 (x\(y\z))\(x\y)\z in I by BCIALG_1:def 18;
then x\(y\z)\z in I by A1,A;
hence thesis by BCIALG_1:7;
end;

theorem TL3422:
(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 A:for x,y,z being Element of X st (x\y)\z in I holds (x\z)\(y\z) in I;
 B: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 A1:(x\y)\z in I & y\z in I;
then (x\z)\(y\z) in I by A;
hence thesis by A1,BCIALG_1:def 18;
end;
0.X in I by BCIALG_1:def 18;
hence thesis by B,Def5;
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
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 Def5;
assume A:for x,y,z being Element of X st (x\y)\z in I
& y\z in I holds x\z in I;
0.X in I by BCIALG_1:def 18;
hence thesis by A,Def5;
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 Def5;
hence thesis by TL3422,TL3421;
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 A1:I c= A & 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;
assume A:(x\y)\y in A;
((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 A1,TL341;
then (x\y)\((x\y)\y) in I by BCIALG_1:7;
hence thesis by A,BCIALG_1:def 18,A1;
end;
hence thesis by TL341;
end;

theorem
 I is implicative-ideal of X implies
I is commutative Ideal of X & I is positive-implicative-ideal of X
proof
assume A:I is implicative-ideal of X;
C1: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;
assume B1:x\y in I;
(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 B2:(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 B2,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 (x\(y\(y\x)))\(y\(x\(y\(y\x))))<=x\y by BCIALG_1:def 11;
hence thesis by P351,A,B1,P141;
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;
assume A1:(x\y)\y in I;
(x\y)\(x\(x\y))\((x\y)\y)=0.X by BCIALG_1:1;
then (x\y)\(x\(x\y))<=((x\y)\y) by BCIALG_1:def 11;
hence thesis by A,P351,P141,A1;
end;
hence thesis by C1,TL251,TL341;
end;