bciideal.miz



    begin

    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;

    theorem :: BCIIDEAL:1

    for x,y,z,u be 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 :: BCIIDEAL:2

    for x,y,z,u be 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));

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

      then (((x \ (y \ z)) \ (x \ (y \ u))) \ (z \ u)) = ( 0. X) by BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIIDEAL:3

    for x,y,z,u,v be 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)));

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

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

      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;

      then (((x \ (y \ (z \ u))) \ (x \ (y \ (z \ v)))) \ (v \ u)) = ( 0. X) by BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIIDEAL:4

    for x,y be 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;

    definition

      let X;

      let a be Element of X;

      :: BCIIDEAL:def1

      func initial_section (a) -> set equals { x where x be Element of X : x <= a };

      coherence ;

    end

    theorem :: BCIIDEAL:5

    

     Th5: x <= a implies x in A

    proof

      assume x <= a;

      then (x \ a) = ( 0. X);

      then (x \ a) in A by BCIALG_1:def 18;

      hence thesis by BCIALG_1:def 18;

    end;

    theorem :: BCIIDEAL:6

    for x,a,b be 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 be Element of X st x = x3 & b <= x3;

      then

       A1: (b \ x) = ( 0. X);

      x in { x1 where x1 be Element of X : x1 is minimal };

      then ex x1 be Element of X st x = x1 & x1 is minimal;

      hence thesis by A1;

    end;

    theorem :: BCIIDEAL:7

    for a be Element of X, x,b be 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 be Element of X st x = x3 & b <= x3;

      then

       A1: (b \ x) = ( 0. X);

      x in { x1 where x1 be Element of X : x1 is minimal };

      then ex x1 be Element of X st x = x1 & x1 is minimal;

      hence thesis by A1;

    end;

    theorem :: BCIIDEAL:8

    ( initial_section a) c= A

    proof

      let b be object;

      assume b in ( initial_section a);

      then ex x1 be Element of X st b = x1 & x1 <= a;

      hence thesis by Th5;

    end;

    theorem :: BCIIDEAL:9

    ( AtomSet X) is Ideal of X implies for x be Element of ( BCK-part X), a be 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 be Element of X st x = x1 & ( 0. X) <= x1;

          then

           A3: (( 0. X) \ x) = ( 0. X);

          x in { x2 where x2 be Element of X : x2 is minimal } by A2, XBOOLE_0:def 4;

          then ex x2 be Element of X st x = x2 & x2 is minimal;

          then ( 0. X) = x by A3;

          hence thesis by TARSKI:def 1;

        end;

      end;

      assume

       A4: P is Ideal of X;

      for x be Element of B, a be 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 :: BCIIDEAL:10

    ( AtomSet X) is Ideal of X implies ( AtomSet X) is closed Ideal of X

    proof

      set P = ( AtomSet X);

      

       A1: for x be 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;

    definition

      let X, I;

      :: BCIIDEAL:def2

      attr I is positive means for x be Element of I holds x is positive;

    end

    theorem :: BCIIDEAL:11

    for X be BCK-algebra, A,I be Ideal of X holds ((A /\ I) = {( 0. X)} iff for x be Element of A, y be 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 be Element of A, y be 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;

        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;

        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 be Element of A, y be Element of I holds (x \ y) = x) implies (A /\ I) = {( 0. X)}

      proof

        assume

         A4: for x be Element of A, y be Element of I holds (x \ y) = x;

        thus (A /\ I) c= {( 0. X)}

        proof

          let x be object;

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

        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;

    theorem :: BCIIDEAL:12

    for X be associative BCI-algebra, A be Ideal of X holds A is closed

    proof

      let X be associative BCI-algebra;

      let A be Ideal of X;

      for x be 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;

    end;

    theorem :: BCIIDEAL:13

    for X be BCI-algebra, A be Ideal of X st X is quasi-associative holds A is closed by BCIALG_1: 71, Th5;

    begin

    definition

      let X be BCI-algebra, IT be Ideal of X;

      :: BCIIDEAL:def3

      attr IT is associative means

      : Def3: ( 0. X) in IT & for x,y,z be 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 be 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 be 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;

      :: BCIIDEAL:def4

      mode associative-ideal of X -> non empty Subset of X means

      : Def4: ( 0. X) in it & for x,y,z be 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 :: BCIIDEAL:14

    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 be 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 :: BCIIDEAL:15

    

     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;

        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;

        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 :: BCIIDEAL:16

    I is associative-ideal of X implies for x be 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 :: BCIIDEAL:17

    (for x be Element of X holds (x \ (( 0. X) \ x)) in I) implies I is closed Ideal of X

    proof

      assume

       A1: for x be Element of X holds (x \ (( 0. X) \ x)) in I;

      for x1 be 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;

      :: BCIIDEAL:def5

      mode p-ideal of X -> non empty Subset of X means

      : Def5: ( 0. X) in it & for x,y,z be 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 :: BCIIDEAL:18

    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 be 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 :: BCIIDEAL:19

    

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

      assume

       A2: x in ( BCK-part X);

      then

       A3: ex x1 be Element of X st x = x1 & ( 0. X) <= x1;

      reconsider x as Element of X by A2;

      (( 0. X) \ x) = ( 0. X) by A3;

      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 :: BCIIDEAL:20

    ( 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 be Element of X st ((x \ z) \ (y \ z)) = c & ( 0. X) <= c by A2;

        then (((x \ z) \ (y \ z)) ` ) = ( 0. X);

        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 be Element of X st y = d & ( 0. X) <= d by A3;

        then (y ` ) = ( 0. X);

        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;

        hence x in A;

      end;

      (( 0. X) \ ( 0. X)) = ( 0. X) by BCIALG_1:def 5;

      then ( 0. X) <= ( 0. X);

      then ( 0. X) in A;

      hence thesis by A1, Def5;

    end;

    theorem :: BCIIDEAL:21

    

     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;

        then ((y \ x) ` ) = (x \ y) by BCIALG_1: 6;

        then ( 0. X) <= (y \ x) by A4;

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

        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 :: BCIIDEAL:22

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

        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

    definition

      let X be BCK-algebra, IT be Ideal of X;

      :: BCIIDEAL:def6

      attr IT is commutative means

      : Def6: for x,y,z be 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 be 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 be Element of X st y = x2 & ( 0. X) <= x2 by A3;

          then

           A4: (y ` ) = ( 0. X);

          ex x1 be Element of X st (x \ y) = x1 & ( 0. X) <= x1 by A2;

          then ((x \ y) ` ) = ( 0. X);

          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;

          hence thesis;

        end;

        

         A5: for x,y,z be 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)));

          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 :: BCIIDEAL:23

    for X be 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 be 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 be Element of X st (x \ y) = x1 & ( 0. X) <= x1 by A2;

        then ((x \ y) ` ) = ( 0. X);

        then

         A4: ((x ` ) \ (y ` )) = ( 0. X) by BCIALG_1: 9;

        ex x2 be Element of X st y = x2 & ( 0. X) <= x2 by A3;

        then ((x ` ) \ ( 0. X)) = ( 0. X) by A4;

        then (( 0. X) \ x) = ( 0. X) by BCIALG_1: 2;

        then ( 0. X) <= x;

        hence thesis;

      end;

      

       A5: for x,y,z be 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)));

        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 :: BCIIDEAL:24

    for X be 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 object;

        assume xx in X1;

        then xx = ( 0. X) by TARSKI:def 1;

        hence thesis;

      end;

      

       A2: for x,y be 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 be 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;

        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 be BCK-algebra holds the carrier of X c= ( BCK-part X)

    proof

      let X be BCK-algebra;

      let x be object;

      assume x in the carrier of X;

      then

      consider x1 be Element of X such that

       A1: x = x1;

      (x1 ` ) = ( 0. X) by BCIALG_1:def 8;

      then ( 0. X) <= x1;

      hence thesis by A1;

    end;

    reserve X for BCK-algebra;

    theorem :: BCIIDEAL:25

    

     Th25: ( BCK-part X) = the carrier of X by Lm1;

    reserve X for BCI-algebra;

    theorem :: BCIIDEAL:26

    (for X be BCI-algebra, x,y be Element of X holds ((x \ y) \ y) = (x \ y)) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y be Element of X holds ((x \ y) \ y) = (x \ y);

      then X is BCK-algebra by BCIALG_1: 13;

      hence thesis by Th25;

    end;

    theorem :: BCIIDEAL:27

    (for X be BCI-algebra, x,y be Element of X holds (x \ (y \ x)) = x) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y be Element of X holds (x \ (y \ x)) = x;

      then X is BCK-algebra by BCIALG_1: 14;

      hence thesis by Th25;

    end;

    theorem :: BCIIDEAL:28

    (for X be BCI-algebra, x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ x))) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y be 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 :: BCIIDEAL:29

    (for X be BCI-algebra, x,y,z be Element of X holds ((x \ y) \ y) = ((x \ z) \ (y \ z))) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y,z be 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 :: BCIIDEAL:30

    (for X be BCI-algebra, x,y be Element of X holds ((x \ y) \ (y \ x)) = (x \ y)) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y be 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 :: BCIIDEAL:31

    (for X be BCI-algebra, x,y be Element of X holds ((x \ y) \ ((x \ y) \ (y \ x))) = ( 0. X)) implies the carrier of X = ( BCK-part X)

    proof

      assume for X be BCI-algebra, x,y be 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 :: BCIIDEAL:32

    for X be 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 be 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 be Element of X st (x \ y) = x1 & ( 0. X) <= x1 by A2;

        then ((x \ y) ` ) = ( 0. X);

        then

         A4: ((x ` ) \ (y ` )) = ( 0. X) by BCIALG_1: 9;

        ex x2 be Element of X st y = x2 & ( 0. X) <= x2 by A3;

        then ((x ` ) \ ( 0. X)) = ( 0. X) by A4;

        then (( 0. X) \ x) = ( 0. X) by BCIALG_1: 2;

        then ( 0. X) <= x;

        hence thesis;

      end;

      

       A5: for x,y,z be 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)));

        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 :: BCIIDEAL:33

    

     Th33: I is commutative Ideal of X iff for x,y be 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 be 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 be Element of X st (x \ y) in I holds (x \ (y \ (y \ x))) in I;

      for x,y,z be 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 :: BCIIDEAL:34

    

     Th34: for I,A be 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 be 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 be 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;

        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 :: BCIIDEAL:35

    

     Th35: (for I be Ideal of X holds I is commutative Ideal of X) iff {( 0. X)} is commutative Ideal of X

    proof

      thus (for I be 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 be 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 be Ideal of X holds {( 0. X)} c= I

        proof

          let I be Ideal of X;

          let x be object;

          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 :: BCIIDEAL:36

    

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

          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 be 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 :: BCIIDEAL:37

    

     Th37: X is commutative BCK-algebra iff for I be Ideal of X holds I is commutative Ideal of X

    proof

      thus X is commutative BCK-algebra implies for I be 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 be 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 :: BCIIDEAL:38

     {( 0. X)} is commutative Ideal of X iff for I be Ideal of X holds I is commutative Ideal of X by Th37, Th36;

    reserve I for Ideal of X;

    theorem :: BCIIDEAL:39

    for x,y be 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));

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

      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 :: BCIIDEAL:40

     {( 0. X)} is commutative Ideal of X iff for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x)) by BCIALG_3: 1, Th36;

    theorem :: BCIIDEAL:41

     {( 0. X)} is commutative Ideal of X iff for x,y be Element of X holds (x \ y) = (x \ (y \ (y \ x))) by BCIALG_3: 3, Th36;

    theorem :: BCIIDEAL:42

     {( 0. X)} is commutative Ideal of X iff for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))) by BCIALG_3: 4, Th36;

    theorem :: BCIIDEAL:43

     {( 0. X)} is commutative Ideal of X iff for x,y be Element of X st x <= y holds x = (y \ (y \ x)) by BCIALG_3: 5, Th36;

    theorem :: BCIIDEAL:44

     {( 0. X)} is commutative Ideal of X implies (for x,y be Element of X holds ((x \ y) = x iff (y \ (y \ x)) = ( 0. X))) & (for x,y be Element of X st (x \ y) = x holds (y \ x) = y) & (for x,y,a be Element of X st y <= a holds ((a \ x) \ (a \ y)) = (y \ x)) & (for x,y be Element of X holds (x \ (y \ (y \ x))) = (x \ y) & ((x \ y) \ ((x \ y) \ x)) = (x \ y)) & for x,y,a be 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 be Element of X holds ((x \ y) = x iff (y \ (y \ x)) = ( 0. X)) by BCIALG_3: 9;

      thus for x,y be Element of X st (x \ y) = x holds (y \ x) = y by A1, BCIALG_3: 7;

      thus for x,y,a be Element of X st y <= a holds ((a \ x) \ (a \ y)) = (y \ x) by A1, BCIALG_3: 8;

      thus for x,y be 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 :: BCIIDEAL:45

    (for I be Ideal of X holds I is commutative Ideal of X) iff for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x)) by BCIALG_3: 1, Th37;

    theorem :: BCIIDEAL:46

    (for I be Ideal of X holds I is commutative Ideal of X) iff for x,y be Element of X holds (x \ y) = (x \ (y \ (y \ x))) by BCIALG_3: 3, Th37;

    theorem :: BCIIDEAL:47

    (for I be Ideal of X holds I is commutative Ideal of X) iff for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))) by BCIALG_3: 4, Th37;

    theorem :: BCIIDEAL:48

    (for I be Ideal of X holds I is commutative Ideal of X) iff for x,y be Element of X st x <= y holds x = (y \ (y \ x)) by BCIALG_3: 5, Th37;

    theorem :: BCIIDEAL:49

    (for I be Ideal of X holds I is commutative Ideal of X) implies (for x,y be Element of X holds ((x \ y) = x iff (y \ (y \ x)) = ( 0. X))) & (for x,y be Element of X st (x \ y) = x holds (y \ x) = y) & (for x,y,a be Element of X st y <= a holds ((a \ x) \ (a \ y)) = (y \ x)) & (for x,y be Element of X holds (x \ (y \ (y \ x))) = (x \ y) & ((x \ y) \ ((x \ y) \ x)) = (x \ y)) & for x,y,a be Element of X st x <= a holds ((a \ y) \ ((a \ y) \ (a \ x))) = ((a \ y) \ (x \ y))

    proof

      assume for I be Ideal of X holds I is commutative Ideal of X;

      then

       A1: X is commutative BCK-algebra by Th37;

      hence for x,y be Element of X holds ((x \ y) = x iff (y \ (y \ x)) = ( 0. X)) by BCIALG_3: 9;

      thus for x,y be Element of X st (x \ y) = x holds (y \ x) = y by A1, BCIALG_3: 7;

      thus for x,y,a be Element of X st y <= a holds ((a \ x) \ (a \ y)) = (y \ x) by A1, BCIALG_3: 8;

      thus for x,y be 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

    definition

      let X be BCK-algebra;

      :: BCIIDEAL:def7

      mode implicative-ideal of X -> non empty Subset of X means

      : Def7: ( 0. X) in it & for x,y,z be 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 :: BCIIDEAL:50

    

     Th50: I is implicative-ideal of X iff for x,y be Element of X st (x \ (y \ x)) in I holds x in I

    proof

      

       A1: (for x,y be 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 be Element of X st (x \ (y \ x)) in I holds x in I;

        

         A3: for x,y,z be 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 be 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;

      :: BCIIDEAL:def8

      mode positive-implicative-ideal of X -> non empty Subset of X means

      : Def8: ( 0. X) in it & for x,y,z be 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 :: BCIIDEAL:51

    

     Th51: I is positive-implicative-ideal of X iff for x,y be 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 be 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 be 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 be Element of X st ((x \ y) \ y) in I holds (x \ y) in I;

        

         A4: for x,y,z be 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));

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

          then ((((x \ z) \ z) \ ((x \ y) \ z)) \ (y \ z)) = ( 0. X) by BCIALG_1: 2;

          then (((x \ z) \ z) \ ((x \ y) \ z)) <= (y \ z);

          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 :: BCIIDEAL:52

    

     Th52: (for x,y,z be Element of X st ((x \ y) \ z) in I & (y \ z) in I holds (x \ z) in I) implies for x,y,z be Element of X st ((x \ y) \ z) in I holds ((x \ z) \ (y \ z)) in I

    proof

      assume

       A1: for x,y,z be 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));

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

      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 :: BCIIDEAL:53

    

     Th53: (for x,y,z be 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 be Element of X st ((x \ y) \ z) in I holds ((x \ z) \ (y \ z)) in I;

      

       A2: for x,y,z be 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 :: BCIIDEAL:54

    I is positive-implicative-ideal of X iff for x,y,z be 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 be 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 be 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 :: BCIIDEAL:55

    I is positive-implicative-ideal of X iff for x,y,z be 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 be 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 :: BCIIDEAL:56

    for I,A be 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 be 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 :: BCIIDEAL:57

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

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

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

        assume (x \ y) in I;

        hence thesis by A1, A4, Th5, Th50;

      end;

      for x,y be 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);

        assume ((x \ y) \ y) in I;

        hence thesis by A1, A5, Th5, Th50;

      end;

      hence thesis by A2, Th33, Th51;

    end;