bcialg_4.miz

    begin

    definition

      struct ( BCIStr_0, ZeroStr) BCIStr_1 (# the carrier -> set,

the ExternalDiff, InternalDiff -> BinOp of the carrier,

the ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for BCIStr_1;

      existence

      proof

        set A = the non empty set, m = the BinOp of A, u = the Element of A;

        take BCIStr_1 (# A, m, m, u #);

        thus the carrier of BCIStr_1 (# A, m, m, u #) is non empty;

        thus thesis;

      end;

    end

    definition

      let A be BCIStr_1;

      let x,y be Element of A;

      :: BCIALG_4:def1

      func x * y -> Element of A equals (the ExternalDiff of A . (x,y));

      coherence ;

    end

    definition

      let IT be non empty BCIStr_1;

      :: BCIALG_4:def2

      attr IT is with_condition_S means

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

    end

    definition

      :: BCIALG_4:def3

      func BCI_S-EXAMPLE -> BCIStr_1 equals BCIStr_1 (# { 0 }, op2 , op2 , op0 #);

      coherence ;

    end

    registration

      cluster BCI_S-EXAMPLE -> strict1 -element;

      coherence ;

    end



     Lm1: BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S by STRUCT_0:def 10;

    registration

      cluster BCI_S-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S;

      coherence by Lm1;

    end

    registration

      cluster strict being_B being_C being_I being_BCI-4 with_condition_S for non empty BCIStr_1;

      existence by Lm1;

    end

    definition

      mode BCI-Algebra_with_Condition(S) is being_B being_C being_I being_BCI-4 with_condition_S non empty BCIStr_1;

    end

    reserve X for non empty BCIStr_1;

    reserve d for Element of X;

    reserve n,m,k for Nat;

    reserve f for sequence of the carrier of X;

    definition

      let X be BCI-Algebra_with_Condition(S);

      let x,y be Element of X;

      :: BCIALG_4:def4

      func Condition_S (x,y) -> non empty Subset of X equals { t where t be Element of X : (t \ x) <= y };

      coherence

      proof

        set a = (( 0. X) \ ((( 0. X) \ x) \ y));

        set Y = { t where t be Element of X : (t \ x) <= y };

         A1:

        now

          let y1 be object;

          assume y1 in Y;

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

          hence y1 in the carrier of X;

        end;

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

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

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

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

        then (a \ x) <= y;

        then a in Y;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: BCIALG_4:1

    for X be BCI-Algebra_with_Condition(S), x,y,u,v be Element of X st u in ( Condition_S (x,y)) & v <= u holds v in ( Condition_S (x,y))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,u,v be Element of X;

      assume that

       A1: u in ( Condition_S (x,y)) and

       A2: v <= u;

      (v \ x) <= (u \ x) by A2, BCIALG_1: 5;

      then

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

      ex u1 be Element of X st u = u1 & (u1 \ x) <= y by A1;

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

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

      then (v \ x) <= y;

      hence thesis;

    end;

    theorem :: BCIALG_4:2

    for X be BCI-Algebra_with_Condition(S) holds for x,y be Element of X holds ex a be Element of ( Condition_S (x,y)) st for z be Element of ( Condition_S (x,y)) holds z <= a

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y be Element of X;

      (((x * y) \ x) \ y) = ((x * y) \ (x * y)) by Def2

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

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

      then (x * y) in { t where t be Element of X : (t \ x) <= y };

      then

      consider u be Element of ( Condition_S (x,y)) such that

       A1: u = (x * y);

      take u;

      for z be Element of ( Condition_S (x,y)) holds z <= u

      proof

        let z be Element of ( Condition_S (x,y));

        z in { t where t be Element of X : (t \ x) <= y };

        then

        consider z1 be Element of X such that

         A2: z = z1 and

         A3: (z1 \ x) <= y;

        (z \ u) = ((z1 \ x) \ y) by A1, A2, Def2

        .= ( 0. X) by A3;

        hence thesis;

      end;

      hence thesis;

    end;



     Lm2: for X be BCI-Algebra_with_Condition(S) holds for x,y be Element of X holds (((x * y) \ x) <= y & for t be Element of X st (t \ x) <= y holds t <= (x * y))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y be Element of X;



       A1: for t be Element of X holds ((t \ x) <= y implies t <= (x * y)) by Def2;

      (((x * y) \ x) \ y) = ((x * y) \ (x * y)) by Def2

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

      hence thesis by A1;

    end;



     Lm3: X is BCI-algebra & (for x,y be Element of X holds (((x * y) \ x) <= y & for t be Element of X st (t \ x) <= y holds t <= (x * y))) implies X is BCI-Algebra_with_Condition(S)

    proof

      assume that

       A1: X is BCI-algebra and

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

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

      proof

        let x,y,z be Element of X;

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

        then

         A3: (((y * z) \ y) \ z) = ( 0. X);

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

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

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

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

        then ((x \ ((x \ y) \ z)) \ y) <= z by A1, BCIALG_1: 2;

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

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

        then

         A4: ((x \ (y * z)) \ ((x \ y) \ z)) = ( 0. X) by A1, BCIALG_1: 7;

        (((x \ y) \ (x \ (y * z))) \ ((y * z) \ y)) = ( 0. X) by A1, BCIALG_1: 11;

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

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

        hence thesis by A1, A4, BCIALG_1:def 7;

      end;

      hence thesis by A1, Def2;

    end;

    theorem :: BCIALG_4:3

    X is BCI-algebra & (for x,y be Element of X holds (((x * y) \ x) <= y & for t be Element of X st (t \ x) <= y holds t <= (x * y))) iff X is BCI-Algebra_with_Condition(S) by Lm2, Lm3;

    definition

      let X be p-Semisimple BCI-algebra;

      :: BCIALG_4:def5

      func Adjoint_pGroup X -> strict AbGroup means the carrier of it = the carrier of X & (for x,y be Element of X holds (the addF of it . (x,y)) = (x \ (( 0. X) \ y))) & ( 0. it ) = ( 0. X);

      existence

      proof

        reconsider A0 = ( 0. X) as Element of X;

        defpred P[ Element of X, Element of X, Element of X] means ex x,y be Element of X st $1 = x & $2 = y & $3 = (x \ (( 0. X) \ y));



         A1: for a,b be Element of X holds ex c be Element of X st P[a, b, c]

        proof

          let a,b be Element of X;

          reconsider x = a, y = b as Element of X;

          reconsider c = (x \ (( 0. X) \ y)) as Element of X;

          take c;

          thus thesis;

        end;

        consider h be BinOp of the carrier of X such that

         A2: for a,b be Element of X holds P[a, b, (h . (a,b))] from BINOP_1:sch 3( A1);

        set G = addLoopStr (# the carrier of X, h, A0 #);



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

        proof

          let x,y be Element of X;

          ex x9,y9 be Element of X st x = x9 & y = y9 & (h . (x,y)) = (x9 \ (( 0. X) \ y9)) by A2;

          hence thesis;

        end;



         A4: for a be Element of X holds ex b be Element of X st ex x be Element of X st a = x & (x \ (( 0. X) \ b)) = ( 0. X) & (b \ (( 0. X) \ x)) = ( 0. X)

        proof

          let a be Element of X;

          reconsider x = a as Element of X;

          reconsider b = (( 0. X) \ x) as Element of X;



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

          take b;

          (x \ (( 0. X) \ b)) = (x \ ((x ` ) ` ))

          .= (x \ x) by BCIALG_1: 54

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

          hence thesis by A5;

        end;

        G is Abelian add-associative right_zeroed right_complementable

        proof

          thus G is Abelian

          proof

            let a,b be Element of G;

            reconsider x = a, y = b as Element of X;



            thus (a + b) = (x \ (( 0. X) \ y)) by A3

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

            .= (b + a) by A3;

          end;

          hereby

            let a,b,c be Element of G;

            reconsider x = a, y = b, z = c as Element of X;



            thus ((a + b) + c) = (h . ((x \ (( 0. X) \ y)),z)) by A3

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

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

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

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

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

            .= (a + (b + c)) by A3;

          end;

          hereby

            let a be Element of G;

            reconsider x = a as Element of X;



            thus (a + ( 0. G)) = (x \ (( 0. X) \ ( 0. X))) by A3

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

            .= a by BCIALG_1: 2;

          end;

          let a be Element of G;

          consider b be Element of X such that

           A6: ex x be Element of X st a = x & (x \ (( 0. X) \ b)) = ( 0. X) & (b \ (( 0. X) \ x)) = ( 0. X) by A4;

          reconsider b as Element of G;

          take b;

          thus thesis by A3, A6;

        end;

        then

        reconsider G as strict AbGroup;

        take G;

        thus thesis by A3;

      end;

      uniqueness

      proof

        thus for G1,G2 be strict AbGroup st the carrier of G1 = the carrier of X & (for x,y be Element of X holds (the addF of G1 . (x,y)) = (x \ (( 0. X) \ y))) & ( 0. G1) = ( 0. X) & the carrier of G2 = the carrier of X & (for x,y be Element of X holds (the addF of G2 . (x,y)) = (x \ (( 0. X) \ y))) & ( 0. G2) = ( 0. X) holds G1 = G2

        proof

          let G1,G2 be strict AbGroup;

          assume that

           A7: the carrier of G1 = the carrier of X and

           A8: for x,y be Element of X holds (the addF of G1 . (x,y)) = (x \ (( 0. X) \ y)) and

           A9: ( 0. G1) = ( 0. X) & the carrier of G2 = the carrier of X and

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

           A11: ( 0. G2) = ( 0. X);

          now

            let a,b be Element of G1;

            reconsider x = a, y = b as Element of X by A7;



            thus (the addF of G1 . (a,b)) = (x \ (( 0. X) \ y)) by A8

            .= (the addF of G2 . (a,b)) by A10;

          end;

          hence thesis by A7, A9, A11, BINOP_1: 2;

        end;

      end;

    end

    ::$Canceled

    theorem :: BCIALG_4:5



     Th4: for X be BCI-algebra holds X is p-Semisimple iff for x,y be Element of X st (x \ y) = ( 0. X) holds x = y

    proof

      let X be BCI-algebra;

      thus X is p-Semisimple implies for x,y be Element of X st (x \ y) = ( 0. X) holds x = y

      proof

        assume

         A1: X is p-Semisimple;

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

        proof

          let x,y be Element of X;

          assume

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

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

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

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

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

          hence thesis by A2, BCIALG_1:def 7;

        end;

        hence thesis;

      end;

      assume

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

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

      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;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:6

    for X be BCI-Algebra_with_Condition(S) st X is p-Semisimple holds for x,y be Element of X holds (x * y) = (x \ (( 0. X) \ y))

    proof

      let X be BCI-Algebra_with_Condition(S);

      assume

       A1: X is p-Semisimple;

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

      proof

        let x,y be Element of X;

        set z1 = (x \ (( 0. X) \ y));

        set z2 = (x * y);

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

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

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

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

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

        then z1 <= z2 by Lm2;

        then

         A2: (z1 \ z2) = ( 0. X);



         A3: for t be Element of X st (t \ x) <= y holds t <= (x \ (( 0. X) \ y))

        proof

          let t be Element of X;

          assume (t \ x) <= y;

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



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

          .= (t \ (x \ (x \ (t \ ( 0. X))))) by A1, BCIALG_1: 57

          .= (t \ (t \ ( 0. X))) by A1

          .= (t \ t) by BCIALG_1: 2

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

          hence thesis;

        end;

        ((x * y) \ x) <= y by Lm2;

        then z2 <= z1 by A3;

        then (z2 \ z1) = ( 0. X);

        hence thesis by A2, BCIALG_1:def 7;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:7



     Th6: for X be BCI-Algebra_with_Condition(S) holds for x,y be Element of X holds (x * y) = (y * x)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y be Element of X;

      ((y * x) \ y) <= x by Lm2;

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

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

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

      then (y * x) <= (x * y) by Lm2;

      then

       A1: ((y * x) \ (x * y)) = ( 0. X);

      ((x * y) \ x) <= y by Lm2;

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

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

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

      then (x * y) <= (y * x) by Lm2;

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

      hence thesis by A1, BCIALG_1:def 7;

    end;

    theorem :: BCIALG_4:8



     Th7: for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds x <= y implies (x * z) <= (y * z) & (z * x) <= (z * y)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;

      assume x <= y;

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

      then

       A1: (((x * z) \ y) \ ((x * z) \ x)) = ( 0. X);

      ((x * z) \ x) <= z by Lm2;

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

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

      then

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

      (x * z) = (z * x) & (y * z) = (z * y) by Th6;

      hence thesis by A2, Lm2;

    end;

    theorem :: BCIALG_4:9



     Th8: for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (( 0. X) * x) = x & (x * ( 0. X)) = x

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x be Element of X;

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

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

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

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

      then x <= (( 0. X) * x) by Lm2;

      then

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

      ((( 0. X) * x) \ ( 0. X)) <= x by Lm2;

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

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

      then (( 0. X) * x) = x by A1, BCIALG_1:def 7;

      hence thesis by Th6;

    end;

    theorem :: BCIALG_4:10



     Th9: for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds ((x * y) * z) = (x * (y * z))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;



       A1: ((z * (x * y)) \ z) <= (x * y) by Lm2;

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

      .= (((z * (x * y)) \ z) \ x) by Th6;

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

      then

       A2: (((((x * y) * z) \ x) \ z) \ ((x * y) \ x)) = ( 0. X);



       A3: ((x * (z * y)) \ x) <= (z * y) by Lm2;

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

      .= (((x * (z * y)) \ x) \ z) by Th6;

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

      then

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

      ((z * y) \ z) <= y by Lm2;

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

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

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

      then (((z * y) * x) \ z) <= (x * y) by Lm2;

      then ((z * y) * x) <= (z * (x * y)) by Lm2;

      then ((y * z) * x) <= (z * (x * y)) by Th6;

      then (x * (y * z)) <= (z * (x * y)) by Th6;

      then (x * (y * z)) <= ((x * y) * z) by Th6;

      then

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

      ((x * y) \ x) <= y by Lm2;

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

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

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

      then (((x * y) * z) \ x) <= (z * y) by Lm2;

      then ((x * y) * z) <= (x * (z * y)) by Lm2;

      then ((x * y) * z) <= (x * (y * z)) by Th6;

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

      hence thesis by A5, BCIALG_1:def 7;

    end;

    theorem :: BCIALG_4:11



     Th10: for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds ((x * y) * z) = ((x * z) * y)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;

      ((x * y) * z) = (x * (y * z)) by Th9

      .= ((y * z) * x) by Th6

      .= (y * (z * x)) by Th9

      .= ((z * x) * y) by Th6;

      hence thesis by Th6;

    end;

    theorem :: BCIALG_4:12



     Th11: for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds ((x \ y) \ z) = (x \ (y * z))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;

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

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

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

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

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

      then (x \ ((x \ y) \ z)) <= (y * z) by Lm2;

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

      then

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

      ((y * z) \ y) <= z by Lm2;

      then (((x \ y) \ (x \ (y * z))) \ ((y * z) \ y)) = ( 0. X) & (((y * z) \ y) \ z) = ( 0. X) by BCIALG_1: 11;

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

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

      hence thesis by A1, BCIALG_1:def 7;

    end;

    theorem :: BCIALG_4:13



     Th12: for X be BCI-Algebra_with_Condition(S) holds for x,y be Element of X holds y <= (x * (y \ x))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y be Element of X;

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

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

      hence thesis by Lm2;

    end;

    theorem :: BCIALG_4:14

    for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds ((x * z) \ (y * z)) <= (x \ y)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;

      x <= (y * (x \ y)) by Th12;

      then (x * z) <= ((y * (x \ y)) * z) by Th7;

      then (x * z) <= ((y * z) * (x \ y)) by Th10;

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

      then

       A1: (((x * z) \ (y * z)) \ (((y * z) * (x \ y)) \ (y * z))) = ( 0. X);

      (((y * z) * (x \ y)) \ (y * z)) <= (x \ y) by Lm2;

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

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

      hence thesis;

    end;

    theorem :: BCIALG_4:15

    for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds (x \ y) <= z iff x <= (y * z) by Th11;

    theorem :: BCIALG_4:16

    for X be BCI-Algebra_with_Condition(S) holds for x,y,z be Element of X holds (x \ y) <= ((x \ z) * (z \ y))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,y,z be Element of X;

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

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

      hence thesis;

    end;



     Lm4: for X be BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is commutative

    proof

      let X be BCI-Algebra_with_Condition(S);

      now

        let a,b be Element of X;



        thus (the ExternalDiff of X . (a,b)) = (a * b)

        .= (b * a) by Th6

        .= (the ExternalDiff of X . (b,a));

      end;

      hence thesis;

    end;



     Lm5: for X be BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is associative

    proof

      let X be BCI-Algebra_with_Condition(S);

      now

        let a,b,c be Element of X;



        thus (the ExternalDiff of X . (a,(the ExternalDiff of X . (b,c)))) = (a * (b * c))

        .= ((a * b) * c) by Th9

        .= (the ExternalDiff of X . ((the ExternalDiff of X . (a,b)),c));

      end;

      hence thesis;

    end;

    registration

      let X be BCI-Algebra_with_Condition(S);

      cluster the ExternalDiff of X -> commutative associative;

      coherence by Lm4, Lm5;

    end

    theorem :: BCIALG_4:17



     Th16: for X be BCI-Algebra_with_Condition(S) holds ( 0. X) is_a_unity_wrt the ExternalDiff of X

    proof

      let X be BCI-Algebra_with_Condition(S);

      now

        let a be Element of X;



        thus (the ExternalDiff of X . (( 0. X),a)) = (( 0. X) * a)

        .= a by Th8;



        thus (the ExternalDiff of X . (a,( 0. X))) = (a * ( 0. X))

        .= a by Th8;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: BCIALG_4:18

    for X be BCI-Algebra_with_Condition(S) holds ( the_unity_wrt the ExternalDiff of X) = ( 0. X)

    proof

      let X be BCI-Algebra_with_Condition(S);

      reconsider e = ( 0. X) as Element of X;

      e is_a_unity_wrt the ExternalDiff of X by Th16;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: BCIALG_4:19



     Th18: for X be BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is having_a_unity

    proof

      let X be BCI-Algebra_with_Condition(S);

      reconsider e = ( 0. X) as Element of X;

      e is_a_unity_wrt the ExternalDiff of X by Th16;

      hence thesis by SETWISEO:def 2;

    end;

    definition

      let X be BCI-Algebra_with_Condition(S);

      :: BCIALG_4:def6

      func power X -> Function of [:the carrier of X, NAT :], the carrier of X means

      : Def6: for h be Element of X holds (it . (h, 0 )) = ( 0. X) & for n holds (it . (h,(n + 1))) = ((it . (h,n)) * h);

      existence

      proof

        defpred P[ object, object] means ex g0 be sequence of the carrier of X, h be Element of X st $1 = h & g0 = $2 & (g0 . 0 ) = ( 0. X) & for n holds (g0 . (n + 1)) = ((g0 . n) * h);



         A1: for x be object st x in the carrier of X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in the carrier of X;

          then

          reconsider b = x as Element of X;

          deffunc F( Nat, Element of X) = ($2 * b);

          consider g0 be sequence of the carrier of X such that

           A2: (g0 . 0 ) = ( 0. X) and

           A3: for n be Nat holds (g0 . (n + 1)) = F(n,.) from NAT_1:sch 12;

          reconsider y = g0 as set;

          take y;

          take g0;

          take b;

          thus x = b & g0 = y & (g0 . 0 ) = ( 0. X) by A2;

          let n;

          thus thesis by A3;

        end;

        consider f be Function such that ( dom f) = the carrier of X and

         A4: for x be object st x in the carrier of X holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        defpred P[ Element of X, Nat, set] means ex g0 be sequence of the carrier of X st g0 = (f . $1) & $3 = (g0 . $2);



         A5: for a be Element of X, n be Nat holds ex b be Element of X st P[a, n, b]

        proof

          let a be Element of X, n be Nat;

          consider g0 be sequence of the carrier of X, h be Element of X such that a = h and

           A6: g0 = (f . a) and (g0 . 0 ) = ( 0. X) and for n holds (g0 . (n + 1)) = ((g0 . n) * h) by A4;

          take (g0 . n), g0;

          thus thesis by A6;

        end;

        consider F be Function of [:the carrier of X, NAT :], the carrier of X such that

         A7: for a be Element of X, n be Nat holds P[a, n, (F . (a,n))] from NAT_1:sch 19( A5);

        take F;

        let h be Element of X;



         A8: ex g2 be sequence of the carrier of X, b be Element of X st h = b & g2 = (f . h) & (g2 . 0 ) = ( 0. X) & for n holds (g2 . (n + 1)) = ((g2 . n) * b) by A4;

        ex g1 be sequence of the carrier of X st g1 = (f . h) & (F . (h, 0 )) = (g1 . 0 ) by A7;

        hence (F . (h, 0 )) = ( 0. X) by A8;

        let n;



         A9: ex g2 be sequence of the carrier of X, b be Element of X st h = b & g2 = (f . h) & (g2 . 0 ) = ( 0. X) & for n holds (g2 . (n + 1)) = ((g2 . n) * b) by A4;

        (ex g0 be sequence of the carrier of X st g0 = (f . h) & (F . (h,n)) = (g0 . n)) & ex g1 be sequence of the carrier of X st g1 = (f . h) & (F . (h,(n + 1))) = (g1 . (n + 1)) by A7;

        hence thesis by A9;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of X, NAT :], the carrier of X;

        assume that

         A10: for h be Element of X holds (f . (h, 0 )) = ( 0. X) & for n holds (f . (h,(n + 1))) = ((f . (h,n)) * h) and

         A11: for h be Element of X holds (g . (h, 0 )) = ( 0. X) & for n holds (g . (h,(n + 1))) = ((g . (h,n)) * h);

        now

          let h be Element of X, n be Nat;

          defpred P[ Nat] means (f . [h, $1]) = (g . [h, $1]);

           A12:

          now

            let n;

            assume

             A13: P[n];



             A14: (g . [h, n]) = (g . (h,n));

            (f . [h, (n + 1)]) = (f . (h,(n + 1)))

            .= ((f . (h,n)) * h) by A10

            .= (g . (h,(n + 1))) by A11, A13, A14

            .= (g . [h, (n + 1)]);

            hence P[(n + 1)];

          end;

          (f . [h, 0 ]) = (f . (h, 0 ))

          .= ( 0. X) by A10

          .= (g . (h, 0 )) by A11

          .= (g . [h, 0 ]);

          then

           A15: P[ 0 ];

          for n holds P[n] from NAT_1:sch 2( A15, A12);

          hence (f . (h,n)) = (g . (h,n));

        end;

        hence thesis;

      end;

    end

    definition

      let X be BCI-Algebra_with_Condition(S);

      let x be Element of X;

      let n be Nat;

      :: BCIALG_4:def7

      func x |^ n -> Element of X equals (( power X) . (x,n));

      correctness ;

    end

    theorem :: BCIALG_4:20

    for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (x |^ 0 ) = ( 0. X) by Def6;

    theorem :: BCIALG_4:21

    for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (x |^ (n + 1)) = ((x |^ n) * x) by Def6;

    theorem :: BCIALG_4:22



     Th21: for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (x |^ 1) = x

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x be Element of X;



      thus (x |^ 1) = (x |^ ( 0 + 1))

      .= ((x |^ 0 ) * x) by Def6

      .= (( 0. X) * x) by Def6

      .= x by Th8;

    end;

    theorem :: BCIALG_4:23



     Th22: for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (x |^ 2) = (x * x)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x be Element of X;



      thus (x |^ 2) = (x |^ (1 + 1))

      .= ((x |^ 1) * x) by Def6

      .= (x * x) by Th21;

    end;

    theorem :: BCIALG_4:24

    for X be BCI-Algebra_with_Condition(S) holds for x be Element of X holds (x |^ 3) = ((x * x) * x)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x be Element of X;



      thus (x |^ 3) = (x |^ (2 + 1))

      .= ((x |^ 2) * x) by Def6

      .= ((x * x) * x) by Th22;

    end;

    theorem :: BCIALG_4:25



     Th24: for X be BCI-Algebra_with_Condition(S) holds (( 0. X) |^ 2) = ( 0. X)

    proof

      let X be BCI-Algebra_with_Condition(S);

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

      then (( 0. X) * ( 0. X)) <= ( 0. X) by Lm2;

      then

       A1: ((( 0. X) * ( 0. X)) \ ( 0. X)) = ( 0. X);

      ( 0. X) <= (( 0. X) * (( 0. X) \ ( 0. X))) by Th12;

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

      then (( 0. X) \ (( 0. X) * ( 0. X))) = ( 0. X);

      then (( 0. X) * ( 0. X)) = ( 0. X) by A1, BCIALG_1:def 7;

      hence thesis by Th22;

    end;



     Lm6: for X be BCI-Algebra_with_Condition(S) holds (( 0. X) |^ (n + 1)) = ( 0. X)

    proof

      let X be BCI-Algebra_with_Condition(S);

      defpred P[ set] means for m holds m = $1 & m <= n implies (( 0. X) |^ (m + 1)) = ( 0. X);

      now

        let k;

        assume

         A1: for m st m = k & m <= n holds (( 0. X) |^ (m + 1)) = ( 0. X);

        let m;

        assume that

         A2: m = (k + 1) and

         A3: m <= n;

        k <= n by A2, A3, NAT_1: 13;

        then

         A4: (( 0. X) |^ (k + 1)) = ( 0. X) by A1;



         A5: (( 0. X) |^ 2) = ( 0. X) by Th24;

        (( 0. X) |^ (m + 1)) = ((( 0. X) |^ (k + 1)) * ( 0. X)) by A2, Def6;

        hence (( 0. X) |^ (m + 1)) = ( 0. X) by A5, A4, Th22;

      end;

      then

       A6: for k st P[k] holds P[(k + 1)];



       A7: P[ 0 ] by Th21;

      for n holds P[n] from NAT_1:sch 2( A7, A6);

      hence thesis;

    end;

    theorem :: BCIALG_4:26

    for X be BCI-Algebra_with_Condition(S) holds (( 0. X) |^ n) = ( 0. X)

    proof

      let X be BCI-Algebra_with_Condition(S);

      defpred P[ set] means for m holds m = $1 & m <= n implies (( 0. X) |^ m) = ( 0. X);



       A1: for k st P[k] holds P[(k + 1)] by Lm6;



       A2: P[ 0 ] by Def6;

      for n holds P[n] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: BCIALG_4:27

    for X be BCI-Algebra_with_Condition(S) holds for x,a be Element of X holds (((x \ a) \ a) \ a) = (x \ (a |^ 3))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,a be Element of X;

      ((x \ a) \ a) = (x \ (a * a)) by Th11;



      then (((x \ a) \ a) \ a) = (x \ ((a * a) * a)) by Th11

      .= (x \ ((a |^ 2) * a)) by Th22

      .= (x \ (a |^ (2 + 1))) by Def6;

      hence thesis;

    end;



     Lm7: for X be BCI-Algebra_with_Condition(S) holds for x,a be Element of X holds ((x,a) to_power 0 ) = (x \ (a |^ 0 ))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,a be Element of X;

      (x \ (a |^ 0 )) = (x \ ( 0. X)) by Def6

      .= x by BCIALG_1: 2;

      hence thesis by BCIALG_2: 1;

    end;

    theorem :: BCIALG_4:28

    for X be BCI-Algebra_with_Condition(S) holds for x,a be Element of X holds ((x,a) to_power n) = (x \ (a |^ n))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,a be Element of X;

      defpred P[ set] means for m holds m = $1 & m <= n implies ((x,a) to_power m) = (x \ (a |^ m));

      now

        let k;

        assume

         A1: for m st m = k & m <= n holds ((x,a) to_power m) = (x \ (a |^ m));

        let m;

        assume that

         A2: m = (k + 1) and

         A3: m <= n;



         A4: ((x,a) to_power m) = (((x,a) to_power k) \ a) & k <= n by A2, A3, BCIALG_2: 4, NAT_1: 13;

        (x \ (a |^ m)) = (x \ ((a |^ k) * a)) by A2, Def6

        .= ((x \ (a |^ k)) \ a) by Th11;

        hence ((x,a) to_power m) = (x \ (a |^ m)) by A1, A4;

      end;

      then

       A5: for k st P[k] holds P[(k + 1)];



       A6: P[ 0 ] by Lm7;

      for n holds P[n] from NAT_1:sch 2( A6, A5);

      hence thesis;

    end;

    definition

      let X be non empty BCIStr_1;

      let F be FinSequence of the carrier of X;

      :: BCIALG_4:def8

      func Product_S F -> Element of X equals (the ExternalDiff of X "**" F);

      correctness ;

    end

    theorem :: BCIALG_4:29

    (the ExternalDiff of X "**" <*d*>) = d

    proof



       A1: ( len <*d*>) = 1 by FINSEQ_1: 39;

      then ex f st (f . 1) = ( <*d*> . 1) & (for n st 0 <> n & n < ( len <*d*>) holds (f . (n + 1)) = (the ExternalDiff of X . ((f . n),( <*d*> . (n + 1))))) & (the ExternalDiff of X "**" <*d*>) = (f . ( len <*d*>)) by FINSOP_1:def 1;

      hence thesis by A1, FINSEQ_1:def 8;

    end;

    theorem :: BCIALG_4:30

    for X be BCI-Algebra_with_Condition(S), F1,F2 be FinSequence of the carrier of X holds ( Product_S (F1 ^ F2)) = (( Product_S F1) * ( Product_S F2)) by Th18, FINSOP_1: 5;

    theorem :: BCIALG_4:31

    for X be BCI-Algebra_with_Condition(S), F be FinSequence of the carrier of X, a be Element of X holds ( Product_S (F ^ <*a*>)) = (( Product_S F) * a) by Th18, FINSOP_1: 4;

    theorem :: BCIALG_4:32

    for X be BCI-Algebra_with_Condition(S), F be FinSequence of the carrier of X, a be Element of X holds ( Product_S ( <*a*> ^ F)) = (a * ( Product_S F)) by Th18, FINSOP_1: 6;

    theorem :: BCIALG_4:33



     Th32: for X be BCI-Algebra_with_Condition(S) holds for a1,a2 be Element of X holds ( Product_S <*a1, a2*>) = (a1 * a2)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let a1,a2 be Element of X;



      thus ( Product_S <*a1, a2*>) = (( Product_S <*a1*>) * a2) by Th18, FINSOP_1: 4

      .= (a1 * a2) by FINSOP_1: 11;

    end;

    theorem :: BCIALG_4:34



     Th33: for X be BCI-Algebra_with_Condition(S) holds for a1,a2,a3 be Element of X holds ( Product_S <*a1, a2, a3*>) = ((a1 * a2) * a3)

    proof

      let X be BCI-Algebra_with_Condition(S);

      let a1,a2,a3 be Element of X;



      thus ( Product_S <*a1, a2, a3*>) = (( Product_S <*a1, a2*>) * a3) by Th18, FINSOP_1: 4

      .= ((a1 * a2) * a3) by FINSOP_1: 12;

    end;

    theorem :: BCIALG_4:35

    for X be BCI-Algebra_with_Condition(S) holds for x,a1,a2 be Element of X holds ((x \ a1) \ a2) = (x \ ( Product_S <*a1, a2*>))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,a1,a2 be Element of X;

      ((x \ a1) \ a2) = (x \ (a1 * a2)) by Th11;

      hence thesis by Th32;

    end;

    theorem :: BCIALG_4:36

    for X be BCI-Algebra_with_Condition(S) holds for x,a1,a2,a3 be Element of X holds (((x \ a1) \ a2) \ a3) = (x \ ( Product_S <*a1, a2, a3*>))

    proof

      let X be BCI-Algebra_with_Condition(S);

      let x,a1,a2,a3 be Element of X;

      (((x \ a1) \ a2) \ a3) = ((x \ (a1 * a2)) \ a3) by Th11

      .= (x \ ((a1 * a2) * a3)) by Th11;

      hence thesis by Th33;

    end;

    theorem :: BCIALG_4:37

    for X be BCI-Algebra_with_Condition(S), a,b be Element of ( AtomSet X) holds for ma be Element of X st (for x be Element of ( BranchV a) holds x <= ma) holds ex mb be Element of X st for y be Element of ( BranchV b) holds y <= mb

    proof

      let X be BCI-Algebra_with_Condition(S);

      let a,b be Element of ( AtomSet X);

      let ma be Element of X;

      assume

       A1: for x be Element of ( BranchV a) holds x <= ma;

      ex mb be Element of X st for y be Element of ( BranchV b) holds y <= mb

      proof

        set mb = ((b * (( 0. X) \ a)) * ma);

        for y be Element of ( BranchV b) holds y <= mb

        proof

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

          then a <= a;

          then a in { yy2 where yy2 be Element of X : a <= yy2 };

          then

           A2: a is Element of ( BranchV a);

          let y be Element of ( BranchV b);

          ( 0. X) in ( AtomSet X);

          then

          consider x0 be Element of ( AtomSet X) such that

           A3: x0 = ( 0. X);

          y in { yy where yy be Element of X : b <= yy };

          then ex yy be Element of X st y = yy & b <= yy;

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

          then (y \ b) in { yy1 where yy1 be Element of X : (b \ b) <= yy1 };

          then

           A4: (y \ b) is Element of ( BranchV (b \ b));



           A5: ((b \ b) \ (x0 \ a)) = (x0 \ (x0 \ a)) by A3, BCIALG_1:def 5

          .= a by BCIALG_1: 24;

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

          then x0 <= x0;

          then x0 in { yy2 where yy2 be Element of X : x0 <= yy2 };

          then x0 is Element of ( BranchV x0);

          then (x0 \ a) is Element of ( BranchV (x0 \ a)) by A2, BCIALG_1: 39;

          then ((y \ b) \ (x0 \ a)) is Element of ( BranchV a) by A4, A5, BCIALG_1: 39;

          then

           A6: ((y \ b) \ (x0 \ a)) <= ma by A1;

          (y \ mb) = ((y \ (b * (( 0. X) \ a))) \ ma) by Th11

          .= (((y \ b) \ (x0 \ a)) \ ma) by A3, Th11

          .= ( 0. X) by A6;

          hence thesis;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      cluster strict being_BCK-5 for BCI-Algebra_with_Condition(S);

      existence by Lm1;

    end

    definition

      mode BCK-Algebra_with_Condition(S) is being_BCK-5 BCI-Algebra_with_Condition(S);

    end

    theorem :: BCIALG_4:38



     Th37: for X be BCK-Algebra_with_Condition(S) holds for x,y be Element of X holds x <= (x * y) & y <= (x * y)

    proof

      let X be BCK-Algebra_with_Condition(S);

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

      proof

        let x,y be Element of X;



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

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



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

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



         A3: ((x \ x) \ y) = (x \ (x * y)) by Th11;

        ((y \ y) \ x) = (y \ (y * x)) by Th11

        .= (y \ (x * y)) by Th6;

        hence thesis by A3, A1, A2;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:39

    for X be BCK-Algebra_with_Condition(S) holds for x,y,z be Element of X holds (((x * y) \ (y * z)) \ (z * x)) = ( 0. X)

    proof

      let X be BCK-Algebra_with_Condition(S);

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

      proof

        let x,y,z be Element of X;

        ((y * x) \ y) <= x by Lm2;

        then

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

        (x * y) = (y * x) by Th6;

        then ((x * y) \ (y * z)) <= (x \ z) by A1, Th11;

        then

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

        ((x \ z) \ (z * x)) = (((x \ z) \ z) \ x) by Th11

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

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

        .= ((z ` ) \ z) by BCIALG_1:def 5

        .= (z ` ) by BCIALG_1:def 8

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

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

        hence thesis by BCIALG_1: 2;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:40

    for X be BCK-Algebra_with_Condition(S) holds for x,y be Element of X holds ((x \ y) * (y \ x)) <= (x * y)

    proof

      let X be BCK-Algebra_with_Condition(S);

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

      proof

        let x,y be Element of X;

        (((x \ y) * (y \ x)) \ (x \ y)) <= (y \ x) by Lm2;

        then

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

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

        .= (x ` ) by BCIALG_1:def 5

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

        then (((x \ y) * (y \ x)) \ ((x \ y) * y)) <= ( 0. X) by A1, Th11;

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

        then

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

        ((y * (x \ y)) \ y) <= (x \ y) by Lm2;

        then

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

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

        .= (y ` ) by BCIALG_1:def 5

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

        then ((y * (x \ y)) \ (y * x)) <= ( 0. X) by A3, Th11;

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

        then

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

        ((x \ y) * y) = (y * (x \ y)) by Th6;

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

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

        hence thesis by Th6;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:41

    for X be BCK-Algebra_with_Condition(S) holds for x be Element of X holds ((x \ ( 0. X)) * (( 0. X) \ x)) = x

    proof

      let X be BCK-Algebra_with_Condition(S);

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

      proof

        let x be Element of X;



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

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

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

        hence thesis by A1, Th8;

      end;

      hence thesis;

    end;

    definition

      let IT be BCK-Algebra_with_Condition(S);

      :: BCIALG_4:def9

      attr IT is commutative means

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

    end

    registration

      cluster commutative for BCK-Algebra_with_Condition(S);

      existence

      proof

        reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);

        IT is commutative by STRUCT_0:def 10;

        hence thesis;

      end;

    end

    theorem :: BCIALG_4:42

    for X be non empty BCIStr_1 holds (X is commutative BCK-Algebra_with_Condition(S) 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) \ z) = (x \ (y * z)))

    proof

      let X be non empty BCIStr_1;

      thus X is commutative BCK-Algebra_with_Condition(S) 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) \ z) = (x \ (y * z))

      proof

        assume

         A1: X is commutative BCK-Algebra_with_Condition(S);

        let x,y,z be Element of X;

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



        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, Th11, BCIALG_1: 2;

      end;

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

      proof

        assume

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



         A4: 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;



         A5: 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 A4

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



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

          .= y by A4;

        end;



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

        proof

          let x be Element of X;

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



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

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

          .= ( 0. X) by A3;

          hence thesis;

        end;



         A7: 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 A6

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

          hence thesis;

        end;



         A8: 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 A4

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

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

          .= ( 0. X) by A7;

          hence thesis;

        end;



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

        proof

          let x,y,z be Element of X;

          assume that

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

           A11: (y \ z) = ( 0. X);

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

          then ((x \ z) \ (x \ y)) = ( 0. X) by A4, A11;

          hence thesis by A4, A10;

        end;



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

        proof

          let x,y,z be Element of X;

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

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

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

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

          then

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

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

          hence thesis by A9, A13;

        end;



         A14: 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;



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

        proof

          let x,y,z be Element of X;

          assume

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

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

          hence thesis by A4, A16;

        end;



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

        proof

          let x,y,z be Element of X;

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

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

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

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

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

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

          hence thesis by A4;

        end;

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

        hence thesis by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7, BCIALG_1:def 8;

      end;

    end;

    theorem :: BCIALG_4:43

    for X be commutative BCK-Algebra_with_Condition(S), a be Element of X st a is greatest holds for x,y be Element of X holds (x * y) = (a \ ((a \ x) \ y))

    proof

      let X be commutative BCK-Algebra_with_Condition(S);

      let a be Element of X;

      assume

       A1: a is greatest;

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

      proof

        let x,y be Element of X;



         A2: (x * y) <= a by A1, BCIALG_2:def 5;

        (a \ ((a \ x) \ y)) = (a \ (a \ (x * y))) by Th11

        .= ((x * y) \ ((x * y) \ a)) by Def9

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

        hence thesis by BCIALG_1: 2;

      end;

      hence thesis;

    end;

    definition

      let X be BCI-algebra;

      let a be Element of X;

      :: BCIALG_4:def10

      func Initial_section (a) -> non empty Subset of X equals { t where t be Element of X : t <= a };

      coherence

      proof

        set Y = { t where t be Element of X : t <= a };

         A1:

        now

          let y1 be object;

          assume y1 in Y;

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

          hence y1 in the carrier of X;

        end;

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

        then a <= a;

        then a in Y;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: BCIALG_4:44

    for X be commutative BCK-Algebra_with_Condition(S), a,b,c be Element of X st ( Condition_S (a,b)) c= ( Initial_section c) holds for x be Element of ( Condition_S (a,b)) holds x <= (c \ ((c \ a) \ b))

    proof

      let X be commutative BCK-Algebra_with_Condition(S);

      let a,b,c be Element of X;

      assume

       A1: ( Condition_S (a,b)) c= ( Initial_section c);

      for x be Element of ( Condition_S (a,b)) holds x <= (c \ ((c \ a) \ b))

      proof

        set u = (c \ ((c \ a) \ b));

        let x be Element of ( Condition_S (a,b));



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

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

        x in { t2 where t2 be Element of X : t2 <= c } by A1, TARSKI:def 3;

        then

        consider x2 be Element of X such that

         A3: x = x2 and

         A4: x2 <= c;



         A5: (x \ (c \ (c \ x))) = (x \ (x \ (x \ c))) by Def9

        .= (x2 \ c) by A3, BCIALG_1: 8

        .= ( 0. X) by A4;

        then

         A6: (((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x))) = ( 0. X) & (x \ u) = ((c \ (c \ x)) \ (c \ ((c \ a) \ b))) by A2, BCIALG_1: 1, BCIALG_1:def 7;

        x in { t1 where t1 be Element of X : (t1 \ a) <= b };

        then

         A7: ex x1 be Element of X st x = x1 & (x1 \ a) <= b;

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

        .= (((c \ (c \ x)) \ a) \ b) by BCIALG_1: 7

        .= ((x \ a) \ b) by A5, A2, BCIALG_1:def 7

        .= ( 0. X) by A7;

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

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let IT be BCK-Algebra_with_Condition(S);

      :: BCIALG_4:def11

      attr IT is positive-implicative means for x,y be Element of IT holds ((x \ y) \ y) = (x \ y);

    end

    registration

      cluster positive-implicative for BCK-Algebra_with_Condition(S);

      existence

      proof

        reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);

        IT is positive-implicative by STRUCT_0:def 10;

        hence thesis;

      end;

    end

    theorem :: BCIALG_4:45



     Th44: for X be BCK-Algebra_with_Condition(S) holds (X is positive-implicative iff for x be Element of X holds (x * x) = x)

    proof

      let X be BCK-Algebra_with_Condition(S);



       A1: X is positive-implicative implies for x be Element of X holds (x * x) = x

      proof

        assume

         A2: X is positive-implicative;

        let x be Element of X;



         A3: ((x * x) \ x) <= x by Lm2;

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

        then ((x * x) \ x) <= (x \ x) by A3, BCIALG_1: 5;

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

        then

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

        (x \ (x * x)) = ((x \ x) \ x) by Th11

        .= (x ` ) by BCIALG_1:def 5

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

        hence thesis by A4, BCIALG_1:def 7;

      end;

      (for x be Element of X holds (x * x) = x) implies X is positive-implicative

      proof

        assume

         A5: for x be Element of X holds (x * x) = x;

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

        proof

          let x,y be Element of X;

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

          hence thesis by Th11;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_4:46



     Th45: for X be BCK-Algebra_with_Condition(S) holds (X is positive-implicative iff for x,y be Element of X holds (x <= y implies (x * y) = y))

    proof

      let X be BCK-Algebra_with_Condition(S);



       A1: X is positive-implicative implies for x,y be Element of X holds (x <= y implies (x * y) = y)

      proof

        assume

         A2: X is positive-implicative;

        let x,y be Element of X;



         A3: ((y * x) \ y) <= x by Lm2;

        ((x * y) \ y) = ((y * x) \ y) by Th6

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

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

        then

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



         A5: (y \ (x * y)) = (y \ (y * x)) by Th6

        .= ((y \ y) \ x) by Th11

        .= (x ` ) by BCIALG_1:def 5

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

        assume x <= y;

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

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

        hence thesis by A5, BCIALG_1:def 7;

      end;

      (for x,y be Element of X holds (x <= y implies (x * y) = y)) implies X is positive-implicative

      proof

        assume

         A6: for x,y be Element of X holds (x <= y implies (x * y) = y);

        for x be Element of X holds (x * x) = x

        proof

          let x be Element of X;

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

          then x <= x;

          hence thesis by A6;

        end;

        hence thesis by Th44;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_4:47



     Th46: for X be BCK-Algebra_with_Condition(S) holds (X is positive-implicative iff for x,y,z be Element of X holds ((x * y) \ z) = ((x \ z) * (y \ z)))

    proof

      let X be BCK-Algebra_with_Condition(S);



       A1: X is positive-implicative implies for x,y,z be Element of X holds ((x * y) \ z) = ((x \ z) * (y \ z))

      proof

        assume

         A2: X is positive-implicative;

        let x,y,z be Element of X;

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

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

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

        then

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

        ((x * y) \ x) <= y by Lm2;

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

        then

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

        ((x * y) \ z) = ((x * y) \ (z * z)) by A2, Th44

        .= (((x * y) \ z) \ z) by Th11;

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

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

        then

         A5: (((x * y) \ z) \ ((x \ z) * (y \ z))) = ( 0. X) by Th11;

        y <= (x * y) by Th37;

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

        then (((x * y) \ z) * (y \ z)) <= (((x * y) \ z) * ((x * y) \ z)) by Th7;

        then

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

        x <= (x * y) by Th37;

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

        then ((x \ z) * (y \ z)) <= (((x * y) \ z) * (y \ z)) by Th7;

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

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

        then (((x \ z) * (y \ z)) \ ((x * y) \ z)) = ( 0. X) by A2, Th44;

        hence thesis by A5, BCIALG_1:def 7;

      end;

      (for x,y,z be Element of X holds ((x * y) \ z) = ((x \ z) * (y \ z))) implies X is positive-implicative

      proof

        assume

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

        for x be Element of X holds (x * x) = x

        proof

          let x be Element of X;

          ((x * x) \ x) = ((x \ x) * (x \ x)) by A7;

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

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

          then

           A8: ((x * x) \ x) = ( 0. X) by Th8;

          (x \ (x * x)) = ((x \ x) \ x) by Th11

          .= (x ` ) by BCIALG_1:def 5

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

          hence thesis by A8, BCIALG_1:def 7;

        end;

        hence thesis by Th44;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_4:48



     Th47: for X be BCK-Algebra_with_Condition(S) holds (X is positive-implicative iff for x,y be Element of X holds (x * y) = (x * (y \ x)))

    proof

      let X be BCK-Algebra_with_Condition(S);



       A1: X is positive-implicative implies for x,y be Element of X holds (x * y) = (x * (y \ x))

      proof

        assume

         A2: X is positive-implicative;

        let x,y be Element of X;

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

        .= (x ` ) by BCIALG_1:def 5

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

        then (y \ x) <= y;

        then (x * (y \ x)) <= (x * y) by Th7;

        then

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

        ((x * y) \ x) = ((x \ x) * (y \ x)) by A2, Th46

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

        .= (y \ x) by Th8;

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

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

        hence thesis by A3, BCIALG_1:def 7;

      end;

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

      proof

        assume

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

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

        proof

          let x,y be Element of X;

          (y * y) = (y * (y \ y)) by A4

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

          .= y by Th8;

          hence thesis by Th11;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: BCIALG_4:49



     Th48: for X be positive-implicative BCK-Algebra_with_Condition(S) holds for x,y be Element of X holds x = ((x \ y) * (x \ (x \ y)))

    proof

      let X be positive-implicative BCK-Algebra_with_Condition(S);

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

      proof

        let x,y be Element of X;

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

        .= (y ` ) by BCIALG_1:def 5

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

        then (x \ y) <= x;

        then x = ((x \ y) * x) by Th45;

        hence thesis by Th47;

      end;

      hence thesis;

    end;

    definition

      let IT be non empty BCIStr_1;

      :: BCIALG_4:def12

      attr IT is being_SB-1 means

      : Def12: for x be Element of IT holds (x * x) = x;

      :: BCIALG_4:def13

      attr IT is being_SB-2 means

      : Def13: for x,y be Element of IT holds (x * y) = (y * x);

      :: BCIALG_4:def14

      attr IT is being_SB-4 means

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

    end



     Lm8: BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S by STRUCT_0:def 10;

    registration

      cluster BCI_S-EXAMPLE -> being_SB-1 being_SB-2 being_SB-4 being_I with_condition_S;

      coherence by Lm8;

    end

    registration

      cluster strict being_SB-1 being_SB-2 being_SB-4 being_I with_condition_S for non empty BCIStr_1;

      existence by Lm8;

    end

    definition

      mode semi-Brouwerian-algebra is being_SB-1 being_SB-2 being_SB-4 being_I with_condition_S non empty BCIStr_1;

    end

    theorem :: BCIALG_4:50

    for X be non empty BCIStr_1 holds (X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra)

    proof

      let X be non empty BCIStr_1;



       A1: X is semi-Brouwerian-algebra implies X is positive-implicative BCK-Algebra_with_Condition(S)

      proof

        assume

         A2: X is semi-Brouwerian-algebra;



         A3: 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

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

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



           A6: x = (x * x) by A2, Def12

          .= ((x \ x) * x) by A2, Def14

          .= (( 0. X) * x) by A2, BCIALG_1:def 5

          .= (y * x) by A2, A5, Def14;

          y = (y * y) by A2, Def12

          .= ((y \ y) * y) by A2, Def14

          .= (y * (y \ y)) by A2, Def13

          .= (y * ( 0. X)) by A2, BCIALG_1:def 5

          .= ((x \ y) * y) by A2, A4, Def13

          .= (x * y) by A2, Def14;

          hence thesis by A2, A6, Def13;

        end;



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

        proof

          let x,y,z be Element of X;

          ((x \ y) \ z) = (x \ (y * z)) by A2, Def2

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

          hence thesis by A2, Def2;

        end;



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

        proof

          let x,y,z be Element of X;

          (((x \ y) \ z) \ ((x \ z) \ y)) = (((x \ y) \ z) \ ((x \ y) \ z)) by A7;

          hence thesis by A2, BCIALG_1:def 5;

        end;



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

        proof

          let x,y be Element of X;

          (x * (y \ x)) = ((y \ x) * x) by A2, Def13

          .= (y * x) by A2, Def14;

          hence thesis by A2, Def13;

        end;



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

        proof

          let x be Element of X;

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

          .= (x \ (x * x)) by A2, Def2

          .= (x \ x) by A2, Def12

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

          hence thesis;

        end;

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

        proof

          let x,y,z be Element of X;

          (((x \ y) \ (z \ y)) \ (x \ z)) = ((x \ (y * (z \ y))) \ (x \ z)) by A2, Def2

          .= ((x \ ((z \ y) * y)) \ (x \ z)) by A2, Def13

          .= ((x \ (z * y)) \ (x \ z)) by A2, Def14

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

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

          .= (y ` ) by A2, BCIALG_1:def 5;

          hence thesis by A10;

        end;

        hence thesis by A2, A10, A3, A8, A9, Th47, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 7, BCIALG_1:def 8;

      end;

      X is positive-implicative BCK-Algebra_with_Condition(S) implies X is semi-Brouwerian-algebra

      proof

        assume

         A11: X is positive-implicative BCK-Algebra_with_Condition(S);



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

        proof

          let x,y be Element of X;

          (y * x) = (y * (x \ y)) by A11, Th47;

          then (x * y) = (y * (x \ y)) by A11, Th6;

          hence thesis by A11, Th6;

        end;

        (for x be Element of X holds (x * x) = x) & for x,y be Element of X holds (x * y) = (y * x) by A11, Th6, Th44;

        hence thesis by A11, A12, Def12, Def13, Def14;

      end;

      hence thesis by A1;

    end;

    definition

      let IT be BCK-Algebra_with_Condition(S);

      :: BCIALG_4:def15

      attr IT is implicative means for x,y be Element of IT holds (x \ (y \ x)) = x;

    end

    registration

      cluster implicative for BCK-Algebra_with_Condition(S);

      existence

      proof

        reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S);

        IT is implicative by STRUCT_0:def 10;

        hence thesis;

      end;

    end

    theorem :: BCIALG_4:51



     Th50: for X be BCK-Algebra_with_Condition(S) holds (X is implicative iff X is commutative & X is positive-implicative)

    proof

      let X be BCK-Algebra_with_Condition(S);

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

      proof

        assume

         A1: X is implicative;



         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;

        end;



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

        proof

          let x,y be Element of X;

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

          then

           A4: ((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 A4, BCIALG_1:def 7;

        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;

          hence thesis by A1;

        end;

        hence thesis by A3;

      end;

      assume that

       A5: X is commutative and

       A6: X is positive-implicative;

      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

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

        ((y \ x) \ ((y \ x) \ x)) = ((y \ x) \ (y \ x)) by A6

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

        hence thesis by A7, BCIALG_1: 2;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_4:52

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

    proof

      let X be BCK-Algebra_with_Condition(S);



       A1: X is implicative implies for x,y,z be Element of X holds (x \ (y \ z)) = (((x \ y) \ z) * (z \ (z \ x)))

      proof

        assume

         A2: X is implicative;

        then

         A3: X is positive-implicative by Th50;

        let x,y,z be Element of X;



         A4: X is commutative by A2, Th50;

        x = ((x \ z) * (x \ (x \ z))) by A3, Th48;

        then

         A5: (x \ (y \ z)) = (((x \ z) * (z \ (z \ x))) \ (y \ z)) by A4;

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

         A6: (((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 A3

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

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

        then

         A7: ((x \ y) \ z) = ((x \ z) \ (y \ z)) by A6, BCIALG_1:def 7;

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

        .= (z \ (z \ x)) by A2;

        hence thesis by A3, A5, A7, Th46;

      end;

      (for x,y,z be Element of X holds (x \ (y \ z)) = (((x \ y) \ z) * (z \ (z \ x)))) implies X is implicative

      proof

        assume

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

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

        proof

          let x,y be Element of X;

          (x \ (y \ x)) = (((x \ y) \ x) * (x \ (x \ x))) by A8

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

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

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

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

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

          hence thesis by Th8;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;