bcialg_3.miz



    begin

    definition

      let IT be non empty BCIStr_0;

      :: BCIALG_3:def1

      attr IT is commutative means

      : Def1: for x,y be Element of IT holds (x \ (x \ y)) = (y \ (y \ x));

    end

    registration

      cluster BCI-EXAMPLE -> commutative;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster commutative for BCK-algebra;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    reserve X for BCK-algebra;

    reserve x,y for Element of X;

    reserve IT for non empty Subset of X;

    theorem :: BCIALG_3:1

    

     Th1: X is commutative BCK-algebra iff for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

    proof

      thus X is commutative BCK-algebra implies for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

      proof

        assume

         A1: X is commutative BCK-algebra;

        let x,y be Element of X;

        (x \ (x \ y)) = (y \ (y \ x)) by A1, Def1;

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

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x));

      for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ x))

      proof

        let x, y;

        (y \ (y \ x)) <= (x \ (x \ y)) by A2;

        then

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

        (x \ (x \ y)) <= (y \ (y \ x)) by A2;

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

        hence thesis by A3, BCIALG_1:def 7;

      end;

      hence thesis by Def1;

    end;

    theorem :: BCIALG_3:2

    

     Th2: for X be BCK-algebra holds for x,y be Element of X holds (x \ (x \ y)) <= y & (x \ (x \ y)) <= x

    proof

      let X be BCK-algebra;

      let x,y be Element of X;

      

       A1: (( 0. X) \ (x \ y)) = ((x \ y) ` )

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

      (((x \ (x \ y)) \ (( 0. X) \ (x \ y))) \ (x \ ( 0. X))) = ( 0. X) by BCIALG_1:def 3;

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

      then ((x \ (x \ y)) \ y) = ( 0. X) & ((x \ (x \ y)) \ x) = ( 0. X) by BCIALG_1: 1, BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIALG_3:3

    

     Th3: X is commutative BCK-algebra iff for x,y be Element of X holds (x \ y) = (x \ (y \ (y \ x)))

    proof

      thus X is commutative BCK-algebra implies for x,y be Element of X holds (x \ y) = (x \ (y \ (y \ x)))

      proof

        assume

         A1: 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 A1, Def1;

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X holds (x \ y) = (x \ (y \ (y \ x)));

      for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

      proof

        let x, y;

        (x \ (x \ (y \ (y \ x)))) <= (y \ (y \ x)) by Th2;

        hence thesis by A2;

      end;

      hence thesis by Th1;

    end;

    theorem :: BCIALG_3:4

    

     Th4: X is commutative BCK-algebra iff for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

    proof

      thus X is commutative BCK-algebra implies for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

      proof

        assume

         A1: X is commutative BCK-algebra;

        let x,y be Element of X;

        (y \ (y \ x)) = (y \ (y \ (x \ (x \ y)))) by A1, Th3;

        hence thesis by A1, Def1;

      end;

      assume

       A2: for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))));

      for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

      proof

        let x, y;

        (x \ (x \ y)) <= x by Th2;

        then

         A3: (y \ x) <= (y \ (x \ (x \ y))) by BCIALG_1: 5;

        (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))) by A2;

        hence thesis by A3, BCIALG_1: 5;

      end;

      hence thesis by Th1;

    end;

    theorem :: BCIALG_3:5

    

     Th5: X is commutative BCK-algebra iff for x,y be Element of X st x <= y holds x = (y \ (y \ x))

    proof

      thus X is commutative BCK-algebra implies for x,y be Element of X st x <= y holds x = (y \ (y \ x))

      proof

        assume

         A1: X is commutative BCK-algebra;

        let x,y be Element of X;

        assume x <= y;

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

        

        then (y \ (y \ x)) = (x \ ( 0. X)) by A1, Def1

        .= x by BCIALG_1: 2;

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X st x <= y holds x = (y \ (y \ x));

      for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

      proof

        let x,y be Element of X;

        ((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

         A3: (y \ x) <= (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;

        then (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))) by A2;

        hence thesis by A3, BCIALG_1: 5;

      end;

      hence thesis by Th1;

    end;

    theorem :: BCIALG_3:6

    

     Th6: for X be non empty BCIStr_0 holds (X is commutative BCK-algebra iff for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = ((y \ z) \ (y \ x)))

    proof

      let X be non empty BCIStr_0;

      thus X is commutative BCK-algebra implies for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = ((y \ z) \ (y \ x))

      proof

        assume

         A1: X is commutative BCK-algebra;

        let x,y,z be Element of X;

        ((x \ (x \ y)) \ z) = ((y \ (y \ x)) \ z) by A1, Def1;

        

        then

         A2: ((x \ z) \ (x \ y)) = ((y \ (y \ x)) \ z) by A1, BCIALG_1: 7

        .= ((y \ z) \ (y \ x)) by A1, BCIALG_1: 7;

        (( 0. X) \ y) = (y ` )

        .= ( 0. X) by A1, BCIALG_1:def 8;

        hence thesis by A1, A2, BCIALG_1: 2;

      end;

      assume

       A3: for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = ((y \ z) \ (y \ x));

      

       A4: for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ x))

      proof

        let x,y be Element of X;

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

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

        .= (y \ (y \ x)) by A3;

        hence thesis;

      end;

      

       A5: for x,y be Element of X holds (x \ ( 0. X)) = x

      proof

        let x,y be Element of X;

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

        hence thesis by A3;

      end;

      for x,y be Element of X holds ((x \ y) = ( 0. X) & (y \ x) = ( 0. X) implies x = y)

      proof

        let x,y be Element of X;

        assume (x \ y) = ( 0. X) & (y \ x) = ( 0. X);

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

        

        then (x \ ( 0. X)) = ((y \ ( 0. X)) \ ( 0. X)) by A5

        .= (y \ ( 0. X)) by A5;

        

        hence x = (y \ ( 0. X)) by A5

        .= y by A5;

      end;

      then

       A6: X is being_BCI-4;

      

       A7: for x be Element of X holds (x \ x) = ( 0. X)

      proof

        let x be Element of X;

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

        

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

        .= (( 0. X) \ (( 0. X) \ x)) by A5

        .= ( 0. X) by A3;

        hence thesis;

      end;

      

       A8: for x be Element of X holds (( 0. X) \ x) = ( 0. X)

      proof

        let x be Element of X;

        ( 0. X) = ((( 0. X) \ x) \ (( 0. X) \ x)) by A7

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

        hence thesis;

      end;

      

       A9: for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X)

      proof

        let x,y,z be Element of X;

        (((x \ y) \ (x \ z)) \ (z \ y)) = (((z \ y) \ (z \ x)) \ (z \ y)) by A3

        .= (((z \ y) \ (z \ x)) \ ((z \ y) \ ( 0. X))) by A5

        .= ((( 0. X) \ (z \ x)) \ (( 0. X) \ (z \ y))) by A3

        .= (( 0. X) \ (( 0. X) \ (z \ y))) by A8

        .= ( 0. X) by A8;

        hence thesis;

      end;

      

       A10: for x,y be Element of X holds ((x \ (x \ y)) \ y) = ( 0. X)

      proof

        let x,y be Element of X;

        ( 0. X) = (((x \ ( 0. X)) \ (x \ y)) \ (y \ ( 0. X))) by A9

        .= ((x \ (x \ y)) \ (y \ ( 0. X))) by A5

        .= ((x \ (x \ y)) \ y) by A5;

        hence thesis;

      end;

      

       A11: X is being_I by A7;

      for x be Element of X holds (x ` ) = ( 0. X) by A8;

      hence thesis by A4, A9, A10, A11, A6, Def1, BCIALG_1: 1, BCIALG_1:def 8;

    end;

    theorem :: BCIALG_3:7

    X is commutative BCK-algebra implies for x,y be Element of X st (x \ y) = x holds (y \ x) = y

    proof

      assume

       A1: X is commutative BCK-algebra;

      let x,y be Element of X;

      assume (x \ y) = x;

      

      then (y \ (y \ x)) = (x \ x) by A1, Def1

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

      

      then (y \ x) = (y \ ( 0. X)) by BCIALG_1: 8

      .= y by BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIALG_3:8

    

     Th8: X is commutative BCK-algebra implies for x,y,a be Element of X st y <= a holds ((a \ x) \ (a \ y)) = (y \ x)

    proof

      assume

       A1: X is commutative BCK-algebra;

      let x,y,a be Element of X;

      assume y <= a;

      then

       A2: (y \ a) = ( 0. X);

      ((a \ x) \ (a \ y)) = ((a \ (a \ y)) \ x) by BCIALG_1: 7

      .= ((y \ ( 0. X)) \ x) by A1, A2, Def1

      .= (y \ x) by BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIALG_3:9

    X is commutative BCK-algebra implies for x,y be Element of X holds ((x \ y) = x iff (y \ (y \ x)) = ( 0. X))

    proof

      assume

       A1: X is commutative BCK-algebra;

      

       A2: for x,y be Element of X holds ((y \ (y \ x)) = ( 0. X) implies (x \ y) = x)

      proof

        let x,y be Element of X;

        assume

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

        (x \ y) = (x \ (x \ (x \ y))) by BCIALG_1: 8

        .= (x \ ( 0. X)) by A1, A3, Def1

        .= x by BCIALG_1: 2;

        hence thesis;

      end;

      for x,y be Element of X holds ((x \ y) = x implies (y \ (y \ x)) = ( 0. X))

      proof

        let x,y be Element of X;

        assume (x \ y) = x;

        

        then (y \ (y \ x)) = (x \ x) by A1, Def1

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

        hence thesis;

      end;

      hence thesis by A2;

    end;

    theorem :: BCIALG_3:10

    X is commutative BCK-algebra implies for x,y be Element of X holds (x \ (y \ (y \ x))) = (x \ y) & ((x \ y) \ ((x \ y) \ x)) = (x \ y)

    proof

      assume

       A1: X is commutative BCK-algebra;

      let x,y be Element of X;

      

       A2: ((x \ y) \ ((x \ y) \ x)) = (x \ (x \ (x \ y))) by A1, Def1

      .= (x \ y) by BCIALG_1: 8;

      (x \ (y \ (y \ x))) = (x \ (x \ (x \ y))) by A1, Def1

      .= (x \ y) by BCIALG_1: 8;

      hence thesis by A2;

    end;

    theorem :: BCIALG_3:11

    X is commutative BCK-algebra implies for x,y,a be Element of X st x <= a holds ((a \ y) \ ((a \ y) \ (a \ x))) = ((a \ y) \ (x \ y)) by Th8;

    definition

      let X be BCI-algebra;

      let a be Element of X;

      :: BCIALG_3:def2

      attr a is being_greatest means for x be Element of X holds (x \ a) = ( 0. X);

      :: BCIALG_3:def3

      attr a is being_positive means (( 0. X) \ a) = ( 0. X);

    end

    begin

    definition

      let IT be BCI-algebra;

      :: BCIALG_3:def4

      attr IT is BCI-commutative means

      : Def4: for x,y be Element of IT st (x \ y) = ( 0. IT) holds x = (y \ (y \ x));

      :: BCIALG_3:def5

      attr IT is BCI-weakly-commutative means

      : Def5: for x,y be Element of IT holds ((x \ (x \ y)) \ (( 0. IT) \ (x \ y))) = (y \ (y \ x));

    end

    registration

      cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster BCI-commutative BCI-weakly-commutative for BCI-algebra;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    theorem :: BCIALG_3:12

    for X be BCI-algebra holds ((ex a be Element of X st a is being_greatest) implies X is BCK-algebra)

    proof

      let X be BCI-algebra;

      given a be Element of X such that

       A1: a is being_greatest;

      for x be Element of X holds (x ` ) = ( 0. X)

      proof

        let x be Element of X;

        (x \ a) = ( 0. X) by A1;

        

        then (x ` ) = ((x \ x) \ a) by BCIALG_1: 7

        .= ( 0. X) by A1;

        hence thesis;

      end;

      hence thesis by BCIALG_1:def 8;

    end;

    theorem :: BCIALG_3:13

    for X be BCI-algebra holds (X is p-Semisimple implies X is BCI-commutative & X is BCI-weakly-commutative)

    proof

      let X be BCI-algebra;

      assume

       A1: X is p-Semisimple;

      

       A2: for x,y be Element of X holds ((x \ (x \ y)) \ (( 0. X) \ (x \ y))) = (y \ (y \ x))

      proof

        let x,y be Element of X;

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

        .= ((( 0. X) \ x) \ (( 0. X) \ y)) by A1, BCIALG_1: 64

        .= ((y \ x) \ (( 0. X) \ ( 0. X))) by A1, BCIALG_1: 58

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

        .= (y \ x) by BCIALG_1: 2;

        hence thesis by A1;

      end;

      for x,y be Element of X st (x \ y) = ( 0. X) holds x = (y \ (y \ x)) by A1;

      hence thesis by A2;

    end;

    theorem :: BCIALG_3:14

    for X be commutative BCK-algebra holds X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra

    proof

      let X be commutative BCK-algebra;

      

       A1: for x,y be Element of X holds ((x \ (x \ y)) \ (( 0. X) \ (x \ y))) = (y \ (y \ x))

      proof

        let x,y be Element of X;

        

         A2: (( 0. X) \ (x \ y)) = ((x \ y) ` )

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

        (x \ (x \ y)) = (y \ (y \ x)) by Def1;

        hence thesis by A2, BCIALG_1: 2;

      end;

      for x,y be Element of X st (x \ y) = ( 0. X) holds x = (y \ (y \ x)) by BCIALG_1:def 11, Th5;

      hence thesis by A1, Def4, Def5;

    end;

    theorem :: BCIALG_3:15

    X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative

    proof

      assume

       A1: X is BCI-weakly-commutative BCI-algebra;

      let x,y be Element of X;

      assume (x \ y) = ( 0. X);

      then ((x \ ( 0. X)) \ (( 0. X) \ ( 0. X))) = (y \ (y \ x)) by A1, Def5;

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

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

      hence thesis by BCIALG_1: 2;

    end;

    theorem :: BCIALG_3:16

    

     Th16: for X be BCI-algebra holds (X is BCI-commutative iff for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))))

    proof

      let X be BCI-algebra;

      

       A1: (for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))) implies X is BCI-commutative

      proof

        assume

         A2: for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))));

        let x,y be Element of X;

        assume (x \ y) = ( 0. X);

        then (x \ (x \ y)) = x by BCIALG_1: 2;

        hence thesis by A2;

      end;

      X is BCI-commutative implies for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

      proof

        assume

         A3: X is BCI-commutative;

        let x,y be Element of X;

        ((x \ (x \ y)) \ y) = ((x \ y) \ (x \ y)) by BCIALG_1: 7

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

        hence thesis by A3;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_3:17

    

     Th17: for X be BCI-algebra holds (X is BCI-commutative iff for x,y be Element of X holds ((x \ (x \ y)) \ (y \ (y \ x))) = (( 0. X) \ (x \ y)))

    proof

      let X be BCI-algebra;

      

       A1: (for x,y be Element of X holds ((x \ (x \ y)) \ (y \ (y \ x))) = (( 0. X) \ (x \ y))) implies X is BCI-commutative

      proof

        assume

         A2: for x,y be Element of X holds ((x \ (x \ y)) \ (y \ (y \ x))) = (( 0. X) \ (x \ y));

        for x,y be Element of X st (x \ y) = ( 0. X) holds x = (y \ (y \ x))

        proof

          let x,y be Element of X;

          

           A3: ((y \ (y \ x)) \ x) = ((y \ x) \ (y \ x)) by BCIALG_1: 7

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

          assume

           A4: (x \ y) = ( 0. X);

          

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

          .= ((x \ ( 0. X)) \ (y \ (y \ x))) by A2, A4

          .= (x \ (y \ (y \ x))) by BCIALG_1: 2;

          hence thesis by A3, BCIALG_1:def 7;

        end;

        hence thesis;

      end;

      X is BCI-commutative implies for x,y be Element of X holds ((x \ (x \ y)) \ (y \ (y \ x))) = (( 0. X) \ (x \ y))

      proof

        assume

         A5: X is BCI-commutative;

        let x,y be Element of X;

        ((x \ (x \ y)) \ (y \ (y \ x))) = ((y \ (y \ (x \ (x \ y)))) \ (y \ (y \ x))) by A5, Th16

        .= ((y \ (y \ (y \ x))) \ (y \ (x \ (x \ y)))) by BCIALG_1: 7

        .= ((y \ x) \ (y \ (x \ (x \ y)))) by BCIALG_1: 8

        .= ((y \ (y \ (x \ (x \ y)))) \ x) by BCIALG_1: 7

        .= ((x \ (x \ y)) \ x) by A5, Th16

        .= ((x \ x) \ (x \ y)) by BCIALG_1: 7;

        hence thesis by BCIALG_1:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_3:18

    for X be BCI-algebra holds (X is BCI-commutative iff for a be Element of ( AtomSet X), x,y be Element of ( BranchV a) holds (x \ (x \ y)) = (y \ (y \ x)))

    proof

      let X be BCI-algebra;

      thus X is BCI-commutative implies for a be Element of ( AtomSet X), x,y be Element of ( BranchV a) holds (x \ (x \ y)) = (y \ (y \ x))

      proof

        assume

         A1: X is BCI-commutative;

        let a be Element of ( AtomSet X);

        let x,y be Element of ( BranchV a);

        (y \ x) in ( BranchV (a \ a)) by BCIALG_1: 39;

        then ex z1 be Element of X st (y \ x) = z1 & (a \ a) <= z1;

        then ( 0. X) <= (y \ x) by BCIALG_1:def 5;

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

        then

         A2: ((y \ (y \ x)) \ (x \ (x \ y))) = ( 0. X) by A1, Th17;

        (x \ y) in ( BranchV (a \ a)) by BCIALG_1: 39;

        then ex z be Element of X st (x \ y) = z & (a \ a) <= z;

        then ( 0. X) <= (x \ y) by BCIALG_1:def 5;

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

        then ((x \ (x \ y)) \ (y \ (y \ x))) = ( 0. X) by A1, Th17;

        hence thesis by A2, BCIALG_1:def 7;

      end;

      assume

       A3: for a be Element of ( AtomSet X), x,y be Element of ( BranchV a) holds (x \ (x \ y)) = (y \ (y \ x));

      for x,y be Element of X holds ((x \ y) = ( 0. X) implies x = (y \ (y \ x)))

      proof

        let x,y be Element of X;

        set aa = (( 0. X) \ (( 0. X) \ x));

        ((aa ` ) ` ) = aa by BCIALG_1: 8;

        then

         A4: aa in ( AtomSet X) by BCIALG_1: 29;

        

         A5: (aa \ x) = ((( 0. X) \ x) \ (( 0. X) \ x)) by BCIALG_1: 7

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

        then

         A6: aa <= x;

        assume

         A7: (x \ y) = ( 0. X);

        then (aa \ y) = ( 0. X) by A5, BCIALG_1: 3;

        then aa <= y;

        then

        consider aa be Element of ( AtomSet X) such that

         A8: aa <= x & aa <= y by A4, A6;

        x in ( BranchV aa) & y in ( BranchV aa) by A8;

        then (x \ (x \ y)) = (y \ (y \ x)) by A3;

        hence thesis by A7, BCIALG_1: 2;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_3:19

    for X be non empty BCIStr_0 holds (X is BCI-commutative BCI-algebra iff for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & (x \ ( 0. X)) = x & (x \ (x \ y)) = (y \ (y \ (x \ (x \ y)))))

    proof

      let X be non empty BCIStr_0;

      (for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & (x \ ( 0. X)) = x & (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))) implies X is BCI-commutative BCI-algebra

      proof

        assume

         A1: for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & (x \ ( 0. X)) = x & (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))));

        for x,y be Element of X holds ((x \ y) = ( 0. X) & (y \ x) = ( 0. X) implies x = y)

        proof

          let x,y be Element of X;

          assume that

           A2: (x \ y) = ( 0. X) and

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

          

           A4: (x \ (x \ y)) = x by A1, A2;

          (y \ (y \ (x \ (x \ y)))) = (y \ ( 0. X)) by A1, A2, A3

          .= y by A1;

          hence thesis by A1, A4;

        end;

        then X is being_BCI-4;

        hence thesis by A1, Th16, BCIALG_1: 11;

      end;

      hence thesis by Th16, BCIALG_1: 1, BCIALG_1: 2;

    end;

    theorem :: BCIALG_3:20

    for X be BCI-algebra holds (X is BCI-commutative iff for x,y,z be Element of X st x <= z & (z \ y) <= (z \ x) holds x <= y)

    proof

      let X be BCI-algebra;

      

       A1: (for x,y,z be Element of X st x <= z & (z \ y) <= (z \ x) holds x <= y) implies X is BCI-commutative

      proof

        assume

         A2: for x,y,z be Element of X st x <= z & (z \ y) <= (z \ x) holds x <= y;

        for x,z be Element of X holds ((x \ z) = ( 0. X) implies x = (z \ (z \ x)))

        proof

          let x,z be Element of X;

          set y = (z \ (z \ x));

          ((z \ y) \ (z \ x)) = ((z \ x) \ (z \ x)) by BCIALG_1: 8

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

          then

           A3: (z \ y) <= (z \ x);

          assume (x \ z) = ( 0. X);

          then x <= z;

          then x <= (z \ (z \ x)) by A2, A3;

          then

           A4: (x \ (z \ (z \ x))) = ( 0. X);

          ((z \ (z \ x)) \ x) = ((z \ x) \ (z \ x)) by BCIALG_1: 7

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

          hence thesis by A4, BCIALG_1:def 7;

        end;

        hence thesis;

      end;

      X is BCI-commutative implies for x,y,z be Element of X st x <= z & (z \ y) <= (z \ x) holds x <= y

      proof

        assume

         A5: X is BCI-commutative;

        for x,y,z be Element of X st x <= z & (z \ y) <= (z \ x) holds x <= y

        proof

          let x,y,z be Element of X;

          assume that

           A6: x <= z and

           A7: (z \ y) <= (z \ x);

          (x \ z) = ( 0. X) by A6;

          then

           A8: x = (z \ (z \ x)) by A5;

          ((z \ y) \ (z \ x)) = ( 0. X) by A7;

          then ( 0. X) = (x \ y) by A8, BCIALG_1: 7;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_3:21

    for X be BCI-algebra holds (X is BCI-commutative iff for x,y,z be Element of X st x <= y & x <= z holds x <= (y \ (y \ z)))

    proof

      let X be BCI-algebra;

      thus X is BCI-commutative implies for x,y,z be Element of X st x <= y & x <= z holds x <= (y \ (y \ z))

      proof

        assume

         A1: X is BCI-commutative;

        for x,y,z be Element of X st x <= y & x <= z holds x <= (y \ (y \ z))

        proof

          let x,y,z be Element of X;

          assume that

           A2: x <= y and

           A3: x <= z;

          

           A4: (x \ z) = ( 0. X) by A3;

          (x \ y) = ( 0. X) by A2;

          then

           A5: x = (y \ (y \ x)) by A1;

          

          then (x \ (y \ (y \ z))) = ((y \ (y \ (y \ z))) \ (y \ x)) by BCIALG_1: 7

          .= ((y \ z) \ (y \ x)) by BCIALG_1: 8

          .= ( 0. X) by A4, A5, BCIALG_1: 7;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A6: for x,y,z be Element of X st x <= y & x <= z holds x <= (y \ (y \ z));

      for x,y be Element of X st (x \ y) = ( 0. X) holds x = (y \ (y \ x))

      proof

        let x,y be Element of X;

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

        then

         A7: x <= x;

        assume (x \ y) = ( 0. X);

        then x <= y;

        then x <= (y \ (y \ x)) by A6, A7;

        then

         A8: (x \ (y \ (y \ x))) = ( 0. X);

        ((y \ (y \ x)) \ x) = ((y \ x) \ (y \ x)) by BCIALG_1: 7

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

        hence thesis by A8, BCIALG_1:def 7;

      end;

      hence thesis;

    end;

    begin

    definition

      let IT be BCK-algebra;

      :: BCIALG_3:def6

      attr IT is bounded means ex a be Element of IT st a is being_greatest;

    end

    registration

      cluster BCI-EXAMPLE -> bounded;

      coherence

      proof

        set IT = BCI-EXAMPLE ;

        set a = the Element of IT;

        IT is bounded

        proof

          take a;

          for x be Element of IT holds (x \ a) = ( 0. IT) by STRUCT_0:def 10;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster bounded commutative for BCK-algebra;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    definition

      let IT be bounded BCK-algebra;

      :: BCIALG_3:def7

      attr IT is involutory means for a be Element of IT st a is being_greatest holds for x be Element of IT holds (a \ (a \ x)) = x;

    end

    theorem :: BCIALG_3:22

    

     Th22: for X be bounded BCK-algebra holds (X is involutory iff for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ y) = ((a \ y) \ (a \ x)))

    proof

      let X be bounded BCK-algebra;

      thus X is involutory implies for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ y) = ((a \ y) \ (a \ x))

      proof

        assume

         A1: X is involutory;

        let a be Element of X;

        assume

         A2: a is being_greatest;

        for x,y be Element of X holds (x \ y) = ((a \ y) \ (a \ x))

        proof

          let x,y be Element of X;

          (x \ y) = ((a \ (a \ x)) \ y) by A1, A2

          .= ((a \ y) \ (a \ x)) by BCIALG_1: 7;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A3: for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ y) = ((a \ y) \ (a \ x));

      let a be Element of X;

      assume

       A4: a is being_greatest;

      now

        let x be Element of X;

        ((a \ (a \ x)) \ ( 0. X)) = ((a \ ( 0. X)) \ (a \ x)) by BCIALG_1: 7

        .= (x \ ( 0. X)) by A3, A4

        .= x by BCIALG_1: 2;

        hence (a \ (a \ x)) = x by BCIALG_1: 2;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_3:23

    

     Th23: for X be bounded BCK-algebra holds (X is involutory iff for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ (a \ y)) = (y \ (a \ x)))

    proof

      let X be bounded BCK-algebra;

      thus X is involutory implies for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ (a \ y)) = (y \ (a \ x))

      proof

        assume

         A1: X is involutory;

        let a be Element of X;

        assume

         A2: a is being_greatest;

        let x,y be Element of X;

        (x \ (a \ y)) = ((a \ (a \ y)) \ (a \ x)) & (y \ (a \ x)) = ((a \ (a \ x)) \ (a \ y)) by A1, A2, Th22;

        hence thesis by BCIALG_1: 7;

      end;

      assume

       A3: for a be Element of X st a is being_greatest holds for x,y be Element of X holds (x \ (a \ y)) = (y \ (a \ x));

      let a be Element of X;

      assume

       A4: a is being_greatest;

      let x be Element of X;

      (a \ (a \ x)) = (x \ (a \ a)) by A3, A4

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

      .= x by BCIALG_1: 2;

      hence thesis;

    end;

    theorem :: BCIALG_3:24

    for X be bounded BCK-algebra holds (X is involutory iff for a be Element of X st a is being_greatest holds for x,y be Element of X holds x <= (a \ y) implies y <= (a \ x))

    proof

      let X be bounded BCK-algebra;

      thus X is involutory implies for a be Element of X st a is being_greatest holds for x,y be Element of X st x <= (a \ y) holds y <= (a \ x) by Th23;

      assume

       A1: for a be Element of X st a is being_greatest holds for x,y be Element of X st x <= (a \ y) holds y <= (a \ x);

      let a be Element of X;

      assume

       A2: a is being_greatest;

      let x be Element of X;

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

      then (a \ x) <= (a \ x);

      then x <= (a \ (a \ x)) by A1, A2;

      then

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

      ((a \ (a \ x)) \ x) = ((a \ x) \ (a \ x)) by BCIALG_1: 7

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

      hence thesis by A3, BCIALG_1:def 7;

    end;

    definition

      let IT be BCK-algebra;

      let a be Element of IT;

      :: BCIALG_3:def8

      attr a is being_Iseki means for x be Element of IT holds (x \ a) = ( 0. IT) & (a \ x) = a;

    end

    definition

      let IT be BCK-algebra;

      :: BCIALG_3:def9

      attr IT is Iseki_extension means ex a be Element of IT st a is being_Iseki;

    end

    registration

      cluster BCI-EXAMPLE -> Iseki_extension;

      coherence

      proof

        set IT = BCI-EXAMPLE ;

        IT is Iseki_extension

        proof

          set a = the Element of IT;

          take a;

          for x be Element of IT holds (x \ a) = ( 0. IT) & (a \ x) = a by STRUCT_0:def 10;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let X be BCK-algebra;

      :: BCIALG_3:def10

      mode Commutative-Ideal of X -> non empty Subset of X means

      : Def10: ( 0. X) in it & for x,y,z be Element of X st ((x \ y) \ z) in it & z in it holds (x \ (y \ (y \ x))) in it ;

      existence

      proof

        set X1 = ( BCK-part X);

        

         A1: 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 X1 by BCIALG_1: 19;

        hence thesis by A1;

      end;

    end

    theorem :: BCIALG_3:25

    IT is Commutative-Ideal of X implies for x,y be Element of X st (x \ y) in IT holds (x \ (y \ (y \ x))) in IT

    proof

      assume

       A1: IT is Commutative-Ideal of X;

      let x,y be Element of X;

      assume (x \ y) in IT;

      then

       A2: ((x \ y) \ ( 0. X)) in IT by BCIALG_1: 2;

      thus thesis by A1, A2, Def10;

    end;

    theorem :: BCIALG_3:26

    

     Th26: for X be BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X

    proof

      let X be BCK-algebra;

      assume

       A1: IT is Commutative-Ideal of X;

      

       A2: for x,y be Element of X st (x \ y) in IT & y in IT holds x in IT

      proof

        let x,y be Element of X;

        assume that

         A3: (x \ y) in IT and

         A4: y in IT;

        

         A5: (x \ (( 0. X) \ (( 0. X) \ x))) = (x \ (( 0. X) \ (x ` )))

        .= (x \ (( 0. X) \ ( 0. X))) by BCIALG_1:def 8

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

        .= x by BCIALG_1: 2;

        ((x \ ( 0. X)) \ y) in IT by A3, BCIALG_1: 2;

        hence thesis by A1, A4, A5, Def10;

      end;

      ( 0. X) in IT by A1, Def10;

      hence thesis by A1, A2, BCIALG_1:def 18;

    end;

    theorem :: BCIALG_3:27

    IT is Commutative-Ideal of X implies for x,y be Element of X st (x \ (x \ y)) in IT holds ((y \ (y \ x)) \ (x \ y)) in IT

    proof

      assume IT is Commutative-Ideal of X;

      then

       A1: IT is Ideal of X by Th26;

      let x,y be Element of X;

      (((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y))) = (((y \ (x \ y)) \ (y \ x)) \ (x \ (x \ y))) by BCIALG_1: 7

      .= ( 0. X) by BCIALG_1: 11;

      then

       A2: ((y \ (y \ x)) \ (x \ y)) <= (x \ (x \ y));

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

      hence thesis by A1, A2, BCIALG_1: 46;

    end;

    begin

    definition

      let IT be BCK-algebra;

      :: BCIALG_3:def11

      attr IT is BCK-positive-implicative means

      : Def11: for x,y,z be Element of IT holds ((x \ y) \ z) = ((x \ z) \ (y \ z));

      :: BCIALG_3:def12

      attr IT is BCK-implicative means

      : Def12: for x,y be Element of IT holds (x \ (y \ x)) = x;

    end

    registration

      cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster Iseki_extension BCK-positive-implicative BCK-implicative bounded commutative for BCK-algebra;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    theorem :: BCIALG_3:28

    

     Th28: X is BCK-positive-implicative BCK-algebra iff for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        let x,y be Element of X;

        ((x \ y) \ y) = ((x \ y) \ (y \ y)) by A1, Def11

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

        .= (x \ y) by BCIALG_1: 2;

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X holds (x \ y) = ((x \ y) \ y);

      for x,y,z be Element of X holds ((x \ y) \ z) = ((x \ z) \ (y \ z))

      proof

        let x,y,z be Element of X;

        ((y \ z) \ y) = ((y \ y) \ z) by BCIALG_1: 7

        .= (z ` ) by BCIALG_1:def 5

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

        then (y \ z) <= y;

        then ((x \ z) \ y) <= ((x \ z) \ (y \ z)) by BCIALG_1: 5;

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

        then

         A3: (((x \ y) \ z) \ ((x \ z) \ (y \ z))) = ( 0. X) by BCIALG_1: 7;

        (((x \ z) \ (y \ z)) \ ((x \ y) \ z)) = ((((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z)) by A2

        .= ((((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y)) by BCIALG_1: 7

        .= ( 0. X) by BCIALG_1:def 3;

        hence thesis by A3, BCIALG_1:def 7;

      end;

      hence thesis by Def11;

    end;

    theorem :: BCIALG_3:29

    

     Th29: X is BCK-positive-implicative BCK-algebra iff for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x))))

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x))))

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x))))

        proof

          let x,y be Element of X;

          ((x \ (x \ y)) \ y) = ((x \ y) \ (x \ y)) by BCIALG_1: 7

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

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

          then

           A2: ((x \ (x \ y)) \ (y \ (y \ x))) <= (y \ (y \ (y \ x))) by BCIALG_1: 5;

          ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) = ((x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y)) by BCIALG_1: 7

          .= ((x \ (y \ (y \ x))) \ (x \ y)) by BCIALG_1: 8

          .= ((x \ (x \ y)) \ (y \ (y \ x))) by BCIALG_1: 7;

          then ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) <= (y \ x) by A2, BCIALG_1: 8;

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

          then

           A3: (((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x))))) = ( 0. X) by BCIALG_1: 7;

          ((y \ (y \ x)) \ x) = ((y \ x) \ (y \ x)) by BCIALG_1: 7

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

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

          then ((y \ (y \ x)) \ (y \ x)) <= (x \ (y \ x)) by BCIALG_1: 5;

          then (y \ (y \ x)) <= (x \ (y \ x)) by A1, Th28;

          then

           A4: ((y \ (y \ x)) \ (x \ (y \ x))) = ( 0. X);

          ((x \ (x \ (y \ (y \ x)))) \ (y \ (y \ x))) = ((x \ (y \ (y \ x))) \ (x \ (y \ (y \ x)))) by BCIALG_1: 7

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

          then ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ x))) = ( 0. X) by A4, BCIALG_1: 3;

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

          then ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x)))) <= ((x \ (y \ x)) \ (x \ (y \ (y \ x)))) by BCIALG_1: 5;

          then ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x)))) <= ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) by BCIALG_1: 7;

          then (x \ (x \ (y \ (y \ x)))) <= ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) by A1, Th28;

          then

           A5: ((x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ (y \ (y \ x)))) \ (y \ x))) = ( 0. X);

          ((y \ (y \ x)) \ y) = ((y \ y) \ (y \ x)) by BCIALG_1: 7

          .= ((y \ x) ` ) by BCIALG_1:def 5

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

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

          then (x \ y) <= (x \ (y \ (y \ x))) by BCIALG_1: 5;

          then (x \ (x \ (y \ (y \ x)))) <= (x \ (x \ y)) by BCIALG_1: 5;

          then ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) <= ((x \ (x \ y)) \ (y \ x)) by BCIALG_1: 5;

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

          then ((x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x))) = ( 0. X) by A5, BCIALG_1: 3;

          hence thesis by A3, BCIALG_1:def 7;

        end;

        hence thesis;

      end;

      assume

       A6: for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x))));

      for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

      proof

        let x,y be Element of X;

        

         A7: ((x \ y) \ ((x \ y) \ (x \ (x \ (x \ y))))) = ((x \ y) \ ((x \ y) \ (x \ y))) by BCIALG_1: 8

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

        .= (x \ y) by BCIALG_1: 2;

        (((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y))) = (((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y))) by BCIALG_1: 7

        .= (((x \ y) \ (y ` )) \ (x \ (x \ y))) by BCIALG_1:def 5

        .= (((x \ y) \ ( 0. X)) \ (x \ (x \ y))) by BCIALG_1:def 8

        .= ((x \ y) \ (x \ (x \ y))) by BCIALG_1: 2

        .= ((x \ (x \ (x \ y))) \ y) by BCIALG_1: 7

        .= ((x \ y) \ y) by BCIALG_1: 8;

        hence thesis by A6, A7;

      end;

      hence thesis by Th28;

    end;

    theorem :: BCIALG_3:30

    X is BCK-positive-implicative BCK-algebra iff for x,y be Element of X holds (x \ y) = ((x \ y) \ (x \ (x \ y)))

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y be Element of X holds (x \ y) = ((x \ y) \ (x \ (x \ y)))

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        let x,y be Element of X;

        

         A2: (((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y))) = (((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y))) by BCIALG_1: 7

        .= (((x \ y) \ (y ` )) \ (x \ (x \ y))) by BCIALG_1:def 5

        .= (((x \ y) \ ( 0. X)) \ (x \ (x \ y))) by BCIALG_1:def 8

        .= ((x \ y) \ (x \ (x \ y))) by BCIALG_1: 2;

        ((x \ y) \ ((x \ y) \ (x \ (x \ (x \ y))))) = ((x \ y) \ ((x \ y) \ (x \ y))) by BCIALG_1: 8

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

        .= (x \ y) by BCIALG_1: 2;

        hence thesis by A1, A2, Th29;

      end;

      assume

       A3: for x,y be Element of X holds (x \ y) = ((x \ y) \ (x \ (x \ y)));

      for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

      proof

        let x,y be Element of X;

        ((x \ y) \ (x \ (x \ y))) = ((x \ (x \ (x \ y))) \ y) by BCIALG_1: 7

        .= ((x \ y) \ y) by BCIALG_1: 8;

        hence thesis by A3;

      end;

      hence thesis by Th28;

    end;

    theorem :: BCIALG_3:31

    X is BCK-positive-implicative BCK-algebra iff for x,y,z be Element of X holds ((x \ z) \ (y \ z)) <= ((x \ y) \ z)

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y,z be Element of X holds ((x \ z) \ (y \ z)) <= ((x \ y) \ z)

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        let x,y,z be Element of X;

        (((x \ z) \ (y \ z)) \ ((x \ y) \ z)) = (((x \ z) \ (y \ z)) \ ((x \ z) \ (y \ z))) by A1, Def11

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

        hence thesis;

      end;

      assume

       A2: for x,y,z be Element of X holds ((x \ z) \ (y \ z)) <= ((x \ y) \ z);

      for x,y,z be Element of X holds ((x \ y) \ z) = ((x \ z) \ (y \ z))

      proof

        let x,y,z be Element of X;

        ((y \ z) \ y) = ((y \ y) \ z) by BCIALG_1: 7

        .= (z ` ) by BCIALG_1:def 5

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

        then (y \ z) <= y;

        then (x \ y) <= (x \ (y \ z)) by BCIALG_1: 5;

        then ((x \ y) \ z) <= ((x \ (y \ z)) \ z) by BCIALG_1: 5;

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

        then

         A3: (((x \ y) \ z) \ ((x \ z) \ (y \ z))) = ( 0. X) by BCIALG_1: 7;

        ((x \ z) \ (y \ z)) <= ((x \ y) \ z) by A2;

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

        hence thesis by A3, BCIALG_1:def 7;

      end;

      hence thesis by Def11;

    end;

    theorem :: BCIALG_3:32

    X is BCK-positive-implicative BCK-algebra iff for x,y be Element of X holds (x \ y) <= ((x \ y) \ y)

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y be Element of X holds (x \ y) <= ((x \ y) \ y)

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        let x,y be Element of X;

        ((x \ y) \ ((x \ y) \ y)) = (((x \ y) \ y) \ ((x \ y) \ y)) by A1, Th28

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

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X holds (x \ y) <= ((x \ y) \ y);

      for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

      proof

        let x,y be Element of X;

        (x \ y) <= ((x \ y) \ y) by A2;

        then

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

        (((x \ y) \ y) \ (x \ y)) = (((x \ y) \ (x \ y)) \ 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;

      hence thesis by Th28;

    end;

    theorem :: BCIALG_3:33

    X is BCK-positive-implicative BCK-algebra iff for x,y be Element of X holds (x \ (x \ (y \ (y \ x)))) <= ((x \ (x \ y)) \ (y \ x))

    proof

      thus X is BCK-positive-implicative BCK-algebra implies for x,y be Element of X holds (x \ (x \ (y \ (y \ x)))) <= ((x \ (x \ y)) \ (y \ x))

      proof

        assume

         A1: X is BCK-positive-implicative BCK-algebra;

        let x,y be Element of X;

        ((x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x))) = ((x \ (x \ (y \ (y \ x)))) \ (x \ (x \ (y \ (y \ x))))) by A1, Th29

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

        hence thesis;

      end;

      assume

       A2: for x,y be Element of X holds (x \ (x \ (y \ (y \ x)))) <= ((x \ (x \ y)) \ (y \ x));

      for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x))))

      proof

        let x,y be Element of X;

        (x \ (x \ (y \ (y \ x)))) <= ((x \ (x \ y)) \ (y \ x)) by A2;

        then

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

        (((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x))))) = ( 0. X) by BCIALG_1: 10;

        hence thesis by A3, BCIALG_1:def 7;

      end;

      hence thesis by Th29;

    end;

    theorem :: BCIALG_3:34

    

     Th34: X is BCK-implicative BCK-algebra iff X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra

    proof

      thus X is BCK-implicative BCK-algebra implies X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        

         A2: for x,y be Element of X holds (x \ (x \ y)) <= (y \ (y \ x))

        proof

          let x,y be Element of X;

          ((x \ (x \ y)) \ y) = ((x \ y) \ (x \ y)) by BCIALG_1: 7

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

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

          then ((x \ (x \ y)) \ (y \ x)) <= (y \ (y \ x)) by BCIALG_1: 5;

          then ((x \ (y \ x)) \ (x \ y)) <= (y \ (y \ x)) by BCIALG_1: 7;

          hence thesis by A1, Def12;

        end;

        for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

        proof

          let x,y be Element of X;

          ((x \ y) \ (y \ (x \ y))) = (x \ y) by A1, Def12;

          hence thesis by A1, Def12;

        end;

        hence thesis by A2, Th1, Th28;

      end;

      assume that

       A3: X is commutative BCK-algebra and

       A4: X is BCK-positive-implicative BCK-algebra;

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

        (x \ (x \ (x \ (y \ x)))) = (x \ (y \ x)) by BCIALG_1: 8;

        then

         A5: (x \ (y \ x)) = (x \ ((y \ x) \ ((y \ x) \ x))) by A3, Def1;

        ((y \ x) \ ((y \ x) \ x)) = ((y \ x) \ (y \ x)) by A4, Th28

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

        hence thesis by A5, BCIALG_1: 2;

      end;

      hence thesis by Def12;

    end;

    theorem :: BCIALG_3:35

    

     Th35: X is BCK-implicative BCK-algebra iff for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x))

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        let x,y be Element of X;

        X is commutative BCK-algebra by A1, Th34;

        

        then ((x \ (x \ y)) \ (x \ y)) = ((y \ (y \ x)) \ (x \ y)) by Def1

        .= ((y \ (x \ y)) \ (y \ x)) by BCIALG_1: 7;

        hence thesis by A1, Def12;

      end;

      assume

       A2: for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x));

      for x,y be Element of X holds ((x \ y) \ y) = (x \ y)

      proof

        let x,y be Element of X;

        

         A3: ((x \ (x \ (x \ y))) \ (x \ (x \ y))) = ((x \ y) \ (x \ (x \ y))) by BCIALG_1: 8

        .= ((x \ (x \ (x \ y))) \ y) by BCIALG_1: 7

        .= ((x \ y) \ y) by BCIALG_1: 8;

        

         A4: ((x \ y) \ x) = ((x \ x) \ y) by BCIALG_1: 7

        .= (y ` ) by BCIALG_1:def 5

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

        ((x \ (x \ (x \ y))) \ (x \ (x \ y))) = ((x \ y) \ ((x \ y) \ x)) by A2;

        hence thesis by A3, A4, BCIALG_1: 2;

      end;

      then

       A5: X is BCK-positive-implicative BCK-algebra by Th28;

      for x,y be Element of X holds (x <= y implies x = (y \ (y \ x)))

      proof

        let x,y be Element of X;

        assume x <= y;

        then

         A6: (x \ y) = ( 0. X);

        

        then (y \ (y \ x)) = ((x \ (x \ y)) \ ( 0. X)) by A2

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

        hence thesis by BCIALG_1: 2;

      end;

      then X is commutative BCK-algebra by Th5;

      hence thesis by A5, Th34;

    end;

    theorem :: BCIALG_3:36

    for X be non empty BCIStr_0 holds (X is BCK-implicative BCK-algebra iff for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = (((y \ z) \ (y \ x)) \ (x \ y)))

    proof

      let X be non empty BCIStr_0;

      thus X is BCK-implicative BCK-algebra implies for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = (((y \ z) \ (y \ x)) \ (x \ y))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        then

         A2: X is commutative BCK-algebra by Th34;

        let x,y,z be Element of X;

        

         A3: (x \ (( 0. X) \ y)) = (x \ (y ` ))

        .= (x \ ( 0. X)) by A1, BCIALG_1:def 8

        .= x by A1, BCIALG_1: 2;

        (((y \ z) \ (y \ x)) \ (x \ y)) = (((y \ z) \ (x \ y)) \ (y \ x)) by A1, BCIALG_1: 7

        .= (((y \ (x \ y)) \ z) \ (y \ x)) by A1, BCIALG_1: 7

        .= ((y \ z) \ (y \ x)) by A1, Def12

        .= ((y \ (y \ x)) \ z) by A1, BCIALG_1: 7

        .= ((x \ (x \ y)) \ z) by A2, Def1

        .= ((x \ z) \ (x \ y)) by A1, BCIALG_1: 7;

        hence thesis by A3;

      end;

      assume

       A4: for x,y,z be Element of X holds (x \ (( 0. X) \ y)) = x & ((x \ z) \ (x \ y)) = (((y \ z) \ (y \ x)) \ (x \ y));

      

       A5: for x,y be Element of X holds (x \ ( 0. X)) = x

      proof

        let x,y be Element of X;

        (( 0. X) \ (( 0. X) \ ( 0. X))) = ( 0. X) by A4;

        hence thesis by A4;

      end;

      

       A6: for x,y be Element of X st (x \ y) = ( 0. X) & (y \ x) = ( 0. X) holds x = y

      proof

        let x,y be Element of X;

        assume (x \ y) = ( 0. X) & (y \ x) = ( 0. X);

        

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

        .= ((y \ ( 0. X)) \ ( 0. X)) by A5;

        

        then (x \ ( 0. X)) = ((y \ ( 0. X)) \ ( 0. X)) by A5

        .= (y \ ( 0. X)) by A5;

        

        hence x = (y \ ( 0. X)) by A5

        .= y by A5;

      end;

      

       A7: for x,y be Element of X holds (x \ (x \ y)) = ((y \ (y \ x)) \ (x \ y))

      proof

        let x,y be Element of X;

        (x \ (x \ y)) = ((x \ ( 0. X)) \ (x \ y)) by A5

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

        hence thesis by A5;

      end;

      

       A8: for y be Element of X holds (y \ y) = ( 0. X)

      proof

        let y be Element of X;

        (( 0. X) \ (( 0. X) \ y)) = ((y \ (y \ ( 0. X))) \ (( 0. X) \ y)) by A7

        .= ((y \ y) \ (( 0. X) \ y)) by A5

        .= (y \ y) by A4;

        hence thesis by A4;

      end;

      

       A9: for x be Element of X holds (( 0. X) \ x) = ( 0. X)

      proof

        let x be Element of X;

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

        hence thesis by A8;

      end;

      

       A10: for x,y be Element of X holds ((x \ y) \ x) = ( 0. X)

      proof

        let x,y be Element of X;

        ((x \ y) \ x) = ((x \ y) \ (x \ ( 0. X))) by A5

        .= (((( 0. X) \ y) \ (( 0. X) \ x)) \ (x \ ( 0. X))) by A4

        .= ((( 0. X) \ (( 0. X) \ x)) \ (x \ ( 0. X))) by A9

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

        hence thesis by A9;

      end;

      

       A11: for x,y,z be Element of X holds (((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x))) = ( 0. X)

      proof

        let x,y,z be Element of X;

        ((((y \ z) \ (y \ x)) \ (x \ y)) \ ((y \ z) \ (y \ x))) = ( 0. X) by A10;

        hence thesis by A4;

      end;

      

       A12: for x,y,z be Element of X holds ((x \ z) \ (x \ y)) = ((y \ z) \ (y \ x))

      proof

        let x,y,z be Element of X;

        (((y \ z) \ (y \ x)) \ ((x \ z) \ (x \ y))) = ( 0. X) & (((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x))) = ( 0. X) by A11;

        hence thesis by A6;

      end;

      then

       A13: X is commutative BCK-algebra by A4, Th6;

      for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x))

      proof

        let x,y be Element of X;

        (x \ (x \ y)) = (y \ (y \ x)) by A13, Def1;

        hence thesis by A7;

      end;

      hence thesis by A4, A12, Th6, Th35;

    end;

    

     Lm1: for X be bounded BCK-algebra holds (X is BCK-implicative implies for a be Element of X st a is being_greatest holds for x be Element of X holds (a \ (a \ x)) = x)

    proof

      let X be bounded BCK-algebra;

      assume X is BCK-implicative;

      then

       A1: X is commutative BCK-algebra by Th34;

      let a be Element of X;

      assume

       A2: a is being_greatest;

      let x be Element of X;

      (a \ (a \ x)) = (x \ (x \ a)) by A1, Def1

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

      hence thesis by BCIALG_1: 2;

    end;

    theorem :: BCIALG_3:37

    

     Th37: for X be bounded BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff X is involutory & X is BCK-positive-implicative)

    proof

      let X be bounded BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies X is involutory & X is BCK-positive-implicative by Lm1, Th34;

      assume that

       A2: X is involutory and

       A3: X is BCK-positive-implicative;

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

        (y \ a) = ( 0. X) by A1;

        then y <= a;

        then

         A4: (y \ x) <= (a \ x) by BCIALG_1: 5;

        (x \ (a \ x)) = ((a \ (a \ x)) \ (a \ x)) by A1, A2

        .= (a \ (a \ x)) by A3, Th28

        .= x by A1, A2;

        then x <= (x \ (y \ x)) by A4, BCIALG_1: 5;

        then

         A5: (x \ (x \ (y \ x))) = ( 0. X);

        ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

        .= ((y \ x) ` ) by BCIALG_1:def 5

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

        hence thesis by A5, BCIALG_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_3:38

    X is BCK-implicative BCK-algebra iff for x,y be Element of X holds (x \ (x \ (y \ x))) = ( 0. X)

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y be Element of X holds (x \ (x \ (y \ x))) = ( 0. X)

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        let x,y be Element of X;

        (x \ (x \ (y \ x))) = (x \ x) by A1, Def12;

        hence thesis by BCIALG_1:def 5;

      end;

      assume

       A2: for x,y be Element of X holds (x \ (x \ (y \ x))) = ( 0. X);

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

        

         A3: ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

        .= ((y \ x) ` ) by BCIALG_1:def 5

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

        (x \ (x \ (y \ x))) = ( 0. X) by A2;

        hence thesis by A3, BCIALG_1:def 7;

      end;

      hence thesis by Def12;

    end;

    theorem :: BCIALG_3:39

    X is BCK-implicative BCK-algebra iff for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        let x,y be Element of X;

        X is commutative BCK-algebra by A1, Th34;

        

        then (y \ (y \ (x \ (x \ y)))) = (y \ (y \ (y \ (y \ x)))) by Def1

        .= (y \ (y \ x)) by BCIALG_1: 8;

        hence thesis by A1, Th35;

      end;

      assume

       A2: for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ (x \ (x \ y))));

      

       A3: for x,y be Element of X holds ((x \ y) \ y) = (x \ y)

      proof

        let x,y be Element of X;

        

         A4: ((x \ y) \ ((x \ y) \ (x \ (x \ (x \ y))))) = ((x \ y) \ ((x \ y) \ (x \ y))) by BCIALG_1: 8

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

        .= (x \ y) by BCIALG_1: 2;

        ((x \ (x \ (x \ y))) \ (x \ (x \ y))) = ((x \ y) \ (x \ (x \ y))) by BCIALG_1: 8

        .= ((x \ (x \ (x \ y))) \ y) by BCIALG_1: 7

        .= ((x \ y) \ y) by BCIALG_1: 8;

        hence thesis by A2, A4;

      end;

      for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ (x \ (x \ y))))

      proof

        let x,y be Element of X;

        (x \ (x \ y)) = ((x \ (x \ y)) \ (x \ y)) by A3;

        hence thesis by A2;

      end;

      then

       A5: X is commutative BCK-algebra by Th4;

      for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x))

      proof

        let x,y be Element of X;

        ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ (x \ (x \ y)))) by A2

        .= (y \ (y \ (y \ (y \ x)))) by A5, Def1;

        hence thesis by BCIALG_1: 8;

      end;

      hence thesis by Th35;

    end;

    theorem :: BCIALG_3:40

    

     Th40: X is BCK-implicative BCK-algebra iff for x,y,z be Element of X holds ((x \ z) \ (x \ y)) = ((y \ z) \ ((y \ x) \ z))

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y,z be Element of X holds ((x \ z) \ (x \ y)) = ((y \ z) \ ((y \ x) \ z))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        then

         A2: X is commutative BCK-algebra by Th34;

        let x,y,z be Element of X;

        

         A3: ((x \ z) \ (x \ y)) = ((x \ (x \ y)) \ z) by BCIALG_1: 7

        .= ((y \ (y \ x)) \ z) by A2, Def1;

        X is BCK-positive-implicative BCK-algebra by A1, Th34;

        hence thesis by A3, Def11;

      end;

      assume

       A4: for x,y,z be Element of X holds ((x \ z) \ (x \ y)) = ((y \ z) \ ((y \ x) \ z));

      

       A5: for x,y be Element of X holds (x \ (x \ y)) = (y \ (y \ x))

      proof

        let x,y be Element of X;

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

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

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

        hence thesis by BCIALG_1: 2;

      end;

      for x,y be Element of X holds ((y \ (y \ x)) \ (y \ x)) = (x \ (x \ y))

      proof

        let x,y be Element of X;

        ((x \ (y \ x)) \ (x \ y)) = ((y \ (y \ x)) \ ((y \ x) \ (y \ x))) by A4;

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

        then ((x \ (y \ x)) \ (x \ y)) = (y \ (y \ x)) by BCIALG_1: 2;

        then ((x \ (x \ y)) \ (y \ x)) = (y \ (y \ x)) by BCIALG_1: 7;

        then ((y \ (y \ x)) \ (y \ x)) = (y \ (y \ x)) by A5;

        hence thesis by A5;

      end;

      then for x,y be Element of X holds ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x));

      hence thesis by Th35;

    end;

    theorem :: BCIALG_3:41

    X is BCK-implicative BCK-algebra iff for x,y,z be Element of X holds (x \ (x \ (y \ z))) = ((y \ z) \ ((y \ z) \ (x \ z)))

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y,z be Element of X holds (x \ (x \ (y \ z))) = ((y \ z) \ ((y \ z) \ (x \ z)))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        then

         A2: X is BCK-positive-implicative BCK-algebra by Th34;

        for x,y,z be Element of X holds (x \ (x \ (y \ z))) = ((y \ z) \ ((y \ z) \ (x \ z)))

        proof

          let x,y,z be Element of X;

          ((x \ ( 0. X)) \ (x \ (y \ z))) = (((y \ z) \ ( 0. X)) \ (((y \ z) \ x) \ ( 0. X))) by A1, Th40;

          

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

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

          

          then (x \ (x \ (y \ z))) = ((y \ z) \ ((y \ z) \ x)) by BCIALG_1: 2

          .= ((y \ z) \ ((y \ x) \ z)) by BCIALG_1: 7;

          hence thesis by A2, Def11;

        end;

        hence thesis;

      end;

      assume

       A3: for x,y,z be Element of X holds (x \ (x \ (y \ z))) = ((y \ z) \ ((y \ z) \ (x \ z)));

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

        (x \ (x \ (y \ x))) = ((y \ x) \ ((y \ x) \ (x \ x))) by A3;

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

        then (x \ (x \ (y \ x))) = ((y \ x) \ (y \ x)) by BCIALG_1: 2;

        then

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

        ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

        .= ((y \ x) ` ) by BCIALG_1:def 5

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

        hence thesis by A4, BCIALG_1:def 7;

      end;

      hence thesis by Def12;

    end;

    theorem :: BCIALG_3:42

    X is BCK-implicative BCK-algebra iff for x,y be Element of X holds (x \ (x \ y)) = ((y \ (y \ x)) \ (x \ y))

    proof

      thus X is BCK-implicative BCK-algebra implies for x,y be Element of X holds (x \ (x \ y)) = ((y \ (y \ x)) \ (x \ y))

      proof

        assume

         A1: X is BCK-implicative BCK-algebra;

        then

         A2: X is commutative BCK-algebra by Th34;

        for x,y be Element of X holds (x \ (x \ y)) = ((y \ (y \ x)) \ (x \ y))

        proof

          let x,y be Element of X;

          ((x \ (x \ y)) \ (x \ y)) = (y \ (y \ x)) by A1, Th35;

          then ((y \ (y \ x)) \ (x \ y)) = (y \ (y \ x)) by A2, Def1;

          hence thesis by A2, Def1;

        end;

        hence thesis;

      end;

      assume

       A3: for x,y be Element of X holds (x \ (x \ y)) = ((y \ (y \ x)) \ (x \ y));

      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 \ ( 0. X)) = ((y \ (y \ x)) \ ( 0. X)) by A3;

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

        hence thesis by BCIALG_1: 2;

      end;

      then

       A4: X is commutative BCK-algebra by Th5;

      for x,y be Element of X holds (x \ y) = ((x \ y) \ y)

      proof

        let x,y be Element of X;

        

         A5: ((x \ y) \ x) = ((x \ x) \ y) by BCIALG_1: 7

        .= (y ` ) by BCIALG_1:def 5

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

        (x \ (x \ (x \ y))) = (((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y))) by A3;

        

        then (x \ (x \ (x \ y))) = ((x \ y) \ (x \ (x \ y))) by A5, BCIALG_1: 2

        .= ((x \ (x \ (x \ y))) \ y) by BCIALG_1: 7

        .= ((x \ y) \ y) by BCIALG_1: 8;

        hence thesis by BCIALG_1: 8;

      end;

      then X is BCK-positive-implicative BCK-algebra by Th28;

      hence thesis by A4, Th34;

    end;

    theorem :: BCIALG_3:43

    

     Th43: for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x be Element of X holds ((a \ x) \ ((a \ x) \ x)) = ( 0. X))

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x be Element of X holds ((a \ x) \ ((a \ x) \ x)) = ( 0. X)

      proof

        assume

         A2: X is BCK-implicative;

        let x be Element of X;

        ((a \ x) \ ((a \ x) \ x)) = (x \ (x \ (a \ x))) by Def1

        .= (x \ x) by A2;

        hence thesis by BCIALG_1:def 5;

      end;

      assume

       A3: for x be Element of X holds ((a \ x) \ ((a \ x) \ x)) = ( 0. X);

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

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

        then

         A4: (x \ (x \ (a \ x))) = ( 0. X) by Def1;

        (y \ a) = ( 0. X) by A1;

        then y <= a;

        then (y \ x) <= (a \ x) by BCIALG_1: 5;

        then

         A5: (x \ (a \ x)) <= (x \ (y \ x)) by BCIALG_1: 5;

        ((x \ (a \ x)) \ x) = ((x \ x) \ (a \ x)) by BCIALG_1: 7

        .= ((a \ x) ` ) by BCIALG_1:def 5

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

        then (x \ (a \ x)) = x by A4, BCIALG_1:def 7;

        then

         A6: (x \ (x \ (y \ x))) = ( 0. X) by A5;

        ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

        .= ((y \ x) ` ) by BCIALG_1:def 5

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

        hence thesis by A6, BCIALG_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_3:44

    for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x be Element of X holds (x \ (a \ x)) = x)

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x be Element of X holds (x \ (a \ x)) = x;

      assume

       A2: for x be Element of X holds (x \ (a \ x)) = x;

      for x,y be Element of X holds (x \ (y \ x)) = x

      proof

        let x,y be Element of X;

        

         A3: ((x \ (a \ x)) \ x) = ((x \ x) \ (a \ x)) by BCIALG_1: 7

        .= ((a \ x) ` ) by BCIALG_1:def 5

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

        (y \ a) = ( 0. X) by A1;

        then y <= a;

        then (y \ x) <= (a \ x) by BCIALG_1: 5;

        then

         A4: (x \ (a \ x)) <= (x \ (y \ x)) by BCIALG_1: 5;

        (x \ (x \ (a \ x))) = (x \ x) by A2

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

        then (x \ (a \ x)) = x by A3, BCIALG_1:def 7;

        then

         A5: (x \ (x \ (y \ x))) = ( 0. X) by A4;

        ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

        .= ((y \ x) ` ) by BCIALG_1:def 5

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

        hence thesis by A5, BCIALG_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_3:45

    for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x be Element of X holds ((a \ x) \ x) = (a \ x))

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x be Element of X holds ((a \ x) \ x) = (a \ x)

      proof

        assume

         A2: X is BCK-implicative;

        let x be Element of X;

        

         A3: (((a \ x) \ x) \ (a \ x)) = (((a \ x) \ (a \ x)) \ x) by BCIALG_1: 7

        .= (x ` ) by BCIALG_1:def 5

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

        ((a \ x) \ ((a \ x) \ x)) = ( 0. X) by A1, A2, Th43;

        hence thesis by A3, BCIALG_1:def 7;

      end;

      assume

       A4: for x be Element of X holds ((a \ x) \ x) = (a \ x);

      let x,y be Element of X;

      ((a \ x) \ ((a \ x) \ x)) = ((a \ x) \ (a \ x)) by A4

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

      then

       A5: (x \ (x \ (a \ x))) = ( 0. X) by Def1;

      (y \ a) = ( 0. X) by A1;

      then y <= a;

      then (y \ x) <= (a \ x) by BCIALG_1: 5;

      then

       A6: (x \ (a \ x)) <= (x \ (y \ x)) by BCIALG_1: 5;

      ((x \ (a \ x)) \ x) = ((x \ x) \ (a \ x)) by BCIALG_1: 7

      .= ((a \ x) ` ) by BCIALG_1:def 5

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

      then (x \ (a \ x)) = x by A5, BCIALG_1:def 7;

      then

       A7: (x \ (x \ (y \ x))) = ( 0. X) by A6;

      ((x \ (y \ x)) \ x) = ((x \ x) \ (y \ x)) by BCIALG_1: 7

      .= ((y \ x) ` ) by BCIALG_1:def 5

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

      hence thesis by A7, BCIALG_1:def 7;

    end;

    theorem :: BCIALG_3:46

    

     Th46: for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x,y be Element of X holds ((a \ y) \ ((a \ y) \ x)) = (x \ y))

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x,y be Element of X holds ((a \ y) \ ((a \ y) \ x)) = (x \ y)

      proof

        assume

         A2: X is BCK-implicative;

        let x,y be Element of X;

        X is involutory by A2, Th37;

        then

         A3: (x \ (a \ y)) = (y \ (a \ x)) by A1, Th23;

        

         A4: ((a \ y) \ ((a \ y) \ x)) = (x \ (x \ (a \ y))) by Def1;

        ((y \ (a \ x)) \ y) = ((y \ y) \ (a \ x)) by BCIALG_1: 7

        .= ((a \ x) ` ) by BCIALG_1:def 5

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

        then (x \ (a \ y)) <= y by A3;

        then (x \ y) <= ((a \ y) \ ((a \ y) \ x)) by A4, BCIALG_1: 5;

        then

         A5: ((x \ y) \ ((a \ y) \ ((a \ y) \ x))) = ( 0. X);

        X is BCK-positive-implicative BCK-algebra by A2, Th34;

        then (a \ y) = ((a \ y) \ y) by Th28;

        then (((a \ y) \ ((a \ y) \ x)) \ (x \ y)) = ( 0. X) by BCIALG_1: 1;

        hence thesis by A5, BCIALG_1:def 7;

      end;

      assume

       A6: for x,y be Element of X holds ((a \ y) \ ((a \ y) \ x)) = (x \ y);

      for x be Element of X holds ((a \ x) \ ((a \ x) \ x)) = ( 0. X)

      proof

        let x be Element of X;

        ((a \ x) \ ((a \ x) \ x)) = (x \ x) by A6;

        hence thesis by BCIALG_1:def 5;

      end;

      hence thesis by A1, Th43;

    end;

    theorem :: BCIALG_3:47

    

     Th47: for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x,y be Element of X holds (y \ (y \ x)) = (x \ (a \ y)))

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x,y be Element of X holds (y \ (y \ x)) = (x \ (a \ y))

      proof

        assume

         A2: X is BCK-implicative;

        let x,y be Element of X;

        (y \ (y \ x)) = (x \ (x \ y)) by Def1

        .= (x \ ((a \ y) \ ((a \ y) \ x))) by A1, A2, Th46

        .= (x \ (x \ (x \ (a \ y)))) by Def1;

        hence thesis by BCIALG_1: 8;

      end;

      assume

       A3: for x,y be Element of X holds (y \ (y \ x)) = (x \ (a \ y));

      for x,y be Element of X holds ((a \ y) \ ((a \ y) \ x)) = (x \ y)

      proof

        let x,y be Element of X;

        ((a \ y) \ ((a \ y) \ x)) = (x \ (a \ (a \ y))) by A3

        .= (x \ (y \ (y \ a))) by Def1

        .= (x \ (y \ ( 0. X))) by A1;

        hence thesis by BCIALG_1: 2;

      end;

      hence thesis by A1, Th46;

    end;

    theorem :: BCIALG_3:48

    for X be bounded commutative BCK-algebra, a be Element of X st a is being_greatest holds (X is BCK-implicative iff for x,y,z be Element of X holds ((x \ (y \ z)) \ (x \ y)) <= (x \ (a \ z)))

    proof

      let X be bounded commutative BCK-algebra;

      let a be Element of X;

      assume

       A1: a is being_greatest;

      thus X is BCK-implicative implies for x,y,z be Element of X holds ((x \ (y \ z)) \ (x \ y)) <= (x \ (a \ z))

      proof

        assume

         A2: X is BCK-implicative;

        let x,y,z be Element of X;

        X is BCK-positive-implicative BCK-algebra by A2, Th34;

        

        then

         A3: (((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ y) \ z)) = (((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ z) \ (y \ z))) by Def11

        .= ( 0. X) by BCIALG_1: 1;

        (((x \ y) \ z) \ (x \ y)) = (((x \ y) \ (x \ y)) \ z) by BCIALG_1: 7

        .= (z ` ) by BCIALG_1:def 5

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

        then

         A4: (((x \ (y \ z)) \ (x \ (x \ z))) \ (x \ y)) = ( 0. X) by A3, BCIALG_1: 3;

        (((x \ (y \ z)) \ (x \ y)) \ (x \ (a \ z))) = (((x \ (y \ z)) \ (x \ y)) \ (z \ (z \ x))) by A1, A2, Th47

        .= (((x \ (y \ z)) \ (x \ y)) \ (x \ (x \ z))) by Def1

        .= ( 0. X) by A4, BCIALG_1: 7;

        hence thesis;

      end;

      assume

       A5: for x,y,z be Element of X holds ((x \ (y \ z)) \ (x \ y)) <= (x \ (a \ z));

      for x be Element of X holds ((a \ x) \ ((a \ x) \ x)) = ( 0. X)

      proof

        let x be Element of X;

        ((x \ (x \ x)) \ (x \ x)) <= (x \ (a \ x)) by A5;

        then ((x \ ( 0. X)) \ (x \ x)) <= (x \ (a \ x)) by BCIALG_1:def 5;

        then (x \ (x \ x)) <= (x \ (a \ x)) by BCIALG_1: 2;

        then (x \ ( 0. X)) <= (x \ (a \ x)) by BCIALG_1:def 5;

        then x <= (x \ (a \ x)) by BCIALG_1: 2;

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

        hence thesis by Def1;

      end;

      hence thesis by A1, Th43;

    end;