bcialg_1.miz



    begin

    definition

      struct ( 1-sorted) BCIStr (# the carrier -> set,

the InternalDiff -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for BCIStr;

      existence

      proof

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

        take BCIStr (# A, m #);

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

        thus thesis;

      end;

    end

    definition

      let A be BCIStr;

      let x,y be Element of A;

      :: BCIALG_1:def1

      func x \ y -> Element of A equals (the InternalDiff of A . (x,y));

      coherence ;

    end

    definition

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

the InternalDiff -> BinOp of the carrier,

the ZeroF -> Element of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for BCIStr_0;

      existence

      proof

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

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

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

        thus thesis;

      end;

    end

    definition

      let IT be non empty BCIStr_0, x be Element of IT;

      :: BCIALG_1:def2

      func x ` -> Element of IT equals (( 0. IT) \ x);

      coherence ;

    end

    definition

      let IT be non empty BCIStr_0;

      :: BCIALG_1:def3

      attr IT is being_B means

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

      :: BCIALG_1:def4

      attr IT is being_C means

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

      :: BCIALG_1:def5

      attr IT is being_I means

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

      :: BCIALG_1:def6

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

      :: BCIALG_1:def7

      attr IT is being_BCI-4 means

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

      :: BCIALG_1:def8

      attr IT is being_BCK-5 means

      : Def8: for x be Element of IT holds (x ` ) = ( 0. IT);

    end

    definition

      :: BCIALG_1:def9

      func BCI-EXAMPLE -> BCIStr_0 equals BCIStr_0 (# { 0 }, op2 , op0 #);

      coherence ;

    end

    registration

      cluster BCI-EXAMPLE -> strict1 -element;

      coherence ;

    end

    registration

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

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster strict being_B being_C being_I being_BCI-4 being_BCK-5 for non empty BCIStr_0;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    definition

      mode BCI-algebra is being_B being_C being_I being_BCI-4 non empty BCIStr_0;

    end

    definition

      mode BCK-algebra is being_BCK-5 BCI-algebra;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_1:def10

      mode SubAlgebra of X -> BCI-algebra means

      : Def10: ( 0. it ) = ( 0. X) & the carrier of it c= the carrier of X & the InternalDiff of it = (the InternalDiff of X || the carrier of it );

      existence

      proof

        take X;

        ( dom the InternalDiff of X) = [:the carrier of X, the carrier of X:] by FUNCT_2:def 1;

        hence thesis;

      end;

    end

    theorem :: BCIALG_1:1

    

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

    proof

      let X be non empty BCIStr_0;

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

      proof

        assume

         A1: X is BCI-algebra;

        now

          let x,y,z be Element of X;

          

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

          

           A3: 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 \ z) \ y)) = ( 0. X) & (((x \ z) \ y) \ ((x \ y) \ z)) = ( 0. X) by A1, Def4;

            hence thesis by A1, Def7;

          end;

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

          hence (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & ((x \ (x \ y)) \ y) = ( 0. X) & (x \ x) = ( 0. X) & ((x \ y) = ( 0. X) & (y \ x) = ( 0. X) implies x = y) by A1, A2, A3, Def5, Def7;

        end;

        hence thesis;

      end;

      assume that

       A4: X is being_I and

       A5: X is being_BCI-4 and

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

      

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

      proof

        let x be Element of X;

        assume

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

        

        then (x ` ) = ((x \ (x \ x)) \ x) by A4

        .= ( 0. X) by A6;

        hence thesis by A5, A8;

      end;

      

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

      proof

        let x be Element of X;

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

        then

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

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

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

        hence thesis by A5, A10;

      end;

      

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

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

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

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

        then ((x \ z) \ (x \ y)) = ( 0. X) by A9, A13;

        hence thesis by A9, A12;

      end;

      

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

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

        then

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

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

        hence thesis by A11, A15;

      end;

      

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

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

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

        hence thesis by A9, A17;

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

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

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

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

        hence thesis by A7;

      end;

      hence thesis by A4, A5, A14, Def3, Def4;

    end;

    definition

      let IT be non empty BCIStr_0;

      let x,y be Element of IT;

      :: BCIALG_1:def11

      pred x <= y means (x \ y) = ( 0. IT);

    end

    reserve X for BCI-algebra;

    reserve x,y,z,u,a,b for Element of X;

    reserve IT for non empty Subset of X;

    

     Lm1: (x \ ( 0. X)) = ( 0. X) implies x = ( 0. X)

    proof

      assume

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

      

      then (x ` ) = ((x \ (x \ x)) \ x) by Def5

      .= ( 0. X) by Th1;

      hence thesis by A1, Def7;

    end;

    theorem :: BCIALG_1:2

    

     Th2: (x \ ( 0. X)) = x

    proof

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

      then

       A1: (x \ (x \ ( 0. X))) = ( 0. X) by Lm1;

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

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

      hence thesis by A1, Def7;

    end;

    theorem :: BCIALG_1:3

    

     Th3: (x \ y) = ( 0. X) & (y \ z) = ( 0. X) implies (x \ z) = ( 0. X)

    proof

      assume that

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

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

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

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

      hence thesis by A1, Th2;

    end;

    theorem :: BCIALG_1:4

    

     Th4: (x \ y) = ( 0. X) implies ((x \ z) \ (y \ z)) = ( 0. X) & ((z \ y) \ (z \ x)) = ( 0. X)

    proof

      assume

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

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

      hence thesis by A1, Th2;

    end;

    theorem :: BCIALG_1:5

    x <= y implies (x \ z) <= (y \ z) & (z \ y) <= (z \ x) by Th4;

    theorem :: BCIALG_1:6

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

    proof

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

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

      hence thesis by Def5;

    end;

    theorem :: BCIALG_1:7

    

     Th7: ((x \ y) \ z) = ((x \ z) \ y)

    proof

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

      then

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

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

      then

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

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

      then

       A3: (((x \ z) \ y) \ ((x \ y) \ z)) = ( 0. X) by A2, Th3;

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

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

      hence thesis by A3, Def7;

    end;

    theorem :: BCIALG_1:8

    

     Th8: (x \ (x \ (x \ y))) = (x \ y)

    proof

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

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

      then

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

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

      hence thesis by A1, Def7;

    end;

    theorem :: BCIALG_1:9

    

     Th9: ((x \ y) ` ) = ((x ` ) \ (y ` ))

    proof

      ((x ` ) \ (y ` )) = ((((x \ y) \ (x \ y)) \ x) \ (y ` )) by Def5

      .= ((((x \ y) \ x) \ (x \ y)) \ (y ` )) by Th7

      .= ((((x \ x) \ y) \ (x \ y)) \ (y ` )) by Th7

      .= (((y ` ) \ (x \ y)) \ (y ` )) by Def5

      .= (((y ` ) \ (y ` )) \ (x \ y)) by Th7;

      hence thesis by Def5;

    end;

    theorem :: BCIALG_1:10

    

     Th10: (((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x))))) = ( 0. X)

    proof

      (((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x))))) = (((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x)) by Th7

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

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

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

      hence thesis by Th1;

    end;

    theorem :: BCIALG_1:11

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

    proof

      let X be non empty BCIStr_0;

      thus X is BCI-algebra implies (X is being_BCI-4 & for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & (x \ ( 0. X)) = x) by Th1, Th2;

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

      proof

        assume that

         A1: X is being_BCI-4 and

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

        

         A3: X is being_I

        proof

          let x be Element of X;

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

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

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

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

          hence thesis by A2;

        end;

        now

          let x,y,z be Element of X;

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

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

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

        end;

        hence thesis by A1, A3, Th1;

      end;

    end;

    theorem :: BCIALG_1:12

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

    proof

      assume

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

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

      proof

        let z be Element of X;

        ((z ` ) ` ) = (z \ (z \ ( 0. X))) by A1;

        then ((z ` ) ` ) = (z \ z) by Th2;

        then (((z ` ) ` ) \ z) = (z ` ) by Def5;

        hence thesis by Th1;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:13

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

    proof

      assume

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

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

      proof

        let z be Element of X;

        ((z ` ) \ ((z ` ) \ z)) = ((z ` ) \ (z ` )) by A1;

        then ((z ` ) \ ((z ` ) \ z)) = ( 0. X) by Def5;

        hence thesis by Th1;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:14

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

    proof

      assume

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

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

      proof

        let z be Element of X;

        ((z \ ( 0. X)) ` ) = ( 0. X) by A1;

        hence thesis by Th2;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:15

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

    proof

      assume

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

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

      proof

        let s be Element of X;

        ((s ` ) \ s) = ((s ` ) \ (s \ s)) by A1;

        then ((s ` ) \ s) = ((s ` ) \ ( 0. X)) by Def5;

        then ((s ` ) \ ((s ` ) \ s)) = ((s ` ) \ (s ` )) by Th2;

        then ((s ` ) \ ((s ` ) \ s)) = ( 0. X) by Def5;

        hence thesis by Th1;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:16

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

    proof

      assume

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

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

      proof

        let s be Element of X;

        ((s ` ) \ (s \ ( 0. X))) = (s ` ) by A1;

        then ((s ` ) \ ((s ` ) \ s)) = ((s ` ) \ (s ` )) by Th2;

        then ((s ` ) \ ((s ` ) \ s)) = ( 0. X) by Def5;

        hence thesis by Th1;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:17

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

    proof

      assume

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

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

      proof

        let s be Element of X;

        ((s ` ) \ ((s ` ) \ (s \ ( 0. X)))) = ( 0. X) by A1;

        then (((s ` ) \ ((s ` ) \ s)) \ s) = (s ` ) by Th2;

        hence thesis by Th1;

      end;

      hence thesis by Def8;

    end;

    theorem :: BCIALG_1:18

    for X be BCI-algebra holds X is being_K iff X is BCK-algebra

    proof

      let X be BCI-algebra;

      thus X is being_K implies X is BCK-algebra

      proof

        assume

         A1: X is being_K;

        now

          let s be Element of X;

          ((s ` ) \ ( 0. X)) = ( 0. X) by A1;

          hence (s ` ) = ( 0. X) by Th2;

        end;

        hence thesis by Def8;

      end;

      assume

       A2: X is BCK-algebra;

      let x,y be Element of X;

      (y ` ) = ( 0. X) by A2, Def8;

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

      hence thesis by Th2;

    end;

    definition

      let X be BCI-algebra;

      :: BCIALG_1:def12

      func BCK-part (X) -> non empty Subset of X equals { x where x be Element of X : ( 0. X) <= x };

      coherence

      proof

        set Y = { x where x be Element of X : ( 0. X) <= x };

         A1:

        now

          let y be object;

          assume y in Y;

          then ex x be Element of X st y = x & ( 0. X) <= x;

          hence y in the carrier of X;

        end;

        (( 0. X) ` ) = ( 0. X) by Def5;

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

        then ( 0. X) in Y;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: BCIALG_1:19

    

     Th19: ( 0. X) in ( BCK-part X)

    proof

      (( 0. X) ` ) = ( 0. X) by Def5;

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

      hence thesis;

    end;

    theorem :: BCIALG_1:20

    for x,y be Element of ( BCK-part X) holds (x \ y) in ( BCK-part X)

    proof

      let x,y be Element of ( BCK-part X);

      x in { x1 where x1 be Element of X : ( 0. X) <= x1 };

      then

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

      y in { y1 where y1 be Element of X : ( 0. X) <= y1 };

      then

       A2: ex y1 be Element of X st y = y1 & ( 0. X) <= y1;

      ((x \ y) ` ) = ((x ` ) \ (y ` )) by Th9;

      then ((x \ y) ` ) = ((y ` ) ` ) by A1;

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

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

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

      hence thesis;

    end;

    theorem :: BCIALG_1:21

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

    proof

      let x be Element of X, y be Element of ( BCK-part X);

      y in { y1 where y1 be Element of X : ( 0. X) <= y1 };

      then ex y1 be Element of X st y = y1 & ( 0. X) <= y1;

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

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

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

      hence thesis;

    end;

    theorem :: BCIALG_1:22

    

     Th22: X is SubAlgebra of X

    proof

      ( dom the InternalDiff of X) = [:the carrier of X, the carrier of X:] by FUNCT_2:def 1;

      then ( 0. X) = ( 0. X) & the InternalDiff of X = (the InternalDiff of X || the carrier of X);

      hence thesis by Def10;

    end;

    definition

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

      :: BCIALG_1:def13

      attr IT is proper means

      : Def13: IT <> X;

    end

    registration

      let X;

      cluster non proper for SubAlgebra of X;

      existence

      proof

        take X;

        X is SubAlgebra of X by Th22;

        hence thesis by Def13;

      end;

    end

    definition

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

      :: BCIALG_1:def14

      attr IT is atom means for z be Element of X holds (z \ IT) = ( 0. X) implies z = IT;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_1:def15

      func AtomSet (X) -> non empty Subset of X equals { x where x be Element of X : x is atom };

      coherence

      proof

        set Y = { x where x be Element of X : x is atom };

         A1:

        now

          let y be object;

          assume y in Y;

          then ex x be Element of X st y = x & x is atom;

          hence y in the carrier of X;

        end;

        for z be Element of X st (z \ ( 0. X)) = ( 0. X) holds z = ( 0. X) by Th2;

        then ( 0. X) is atom;

        then ( 0. X) in Y;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: BCIALG_1:23

    

     Th23: ( 0. X) in ( AtomSet X)

    proof

      for z be Element of X st (z \ ( 0. X)) = ( 0. X) holds z = ( 0. X) by Th2;

      then ( 0. X) is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:24

    

     Th24: for x be Element of X holds x in ( AtomSet X) iff for z be Element of X holds (z \ (z \ x)) = x

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for z be Element of X holds (z \ (z \ x)) = x

      proof

        assume x in ( AtomSet X);

        then

         A1: ex x1 be Element of X st x = x1 & x1 is atom;

        let z be Element of X;

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

        hence thesis by A1;

      end;

      assume

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

      now

        let z be Element of X;

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

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

        hence z = x by Th2;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:25

    for x be Element of X holds x in ( AtomSet X) iff for u,z be Element of X holds ((z \ u) \ (z \ x)) = (x \ u)

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for u,z be Element of X holds ((z \ u) \ (z \ x)) = (x \ u)

      proof

        assume x in ( AtomSet X);

        then

         A1: ex x1 be Element of X st x = x1 & x1 is atom;

        let u,z be Element of X;

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

        then (z \ (z \ x)) = x by A1;

        hence thesis by Th7;

      end;

      assume

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

      now

        let z be Element of X;

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

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

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

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

        hence z = x by Th2;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:26

    for x be Element of X holds x in ( AtomSet X) iff for y,z be Element of X holds (x \ (z \ y)) <= (y \ (z \ x))

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for y,z be Element of X holds (x \ (z \ y)) <= (y \ (z \ x))

      proof

        assume x in ( AtomSet X);

        then

         A1: ex x1 be Element of X st x = x1 & x1 is atom;

        let y,z be Element of X;

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

        then ((x \ (z \ y)) \ (y \ (z \ x))) = (((z \ (z \ x)) \ (z \ y)) \ (y \ (z \ x))) by A1;

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

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

        then ((x \ (z \ y)) \ (y \ (z \ x))) = ((((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x))) \ ((z \ (z \ y)) \ y)) by Th1;

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

        hence thesis;

      end;

      assume

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

      now

        let z be Element of X;

        assume

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

        (x \ (z \ ( 0. X))) <= ((z \ x) ` ) by A2;

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

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

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

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

        hence z = x by A3, Def7;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:27

    for x be Element of X holds x in ( AtomSet X) iff for y,z,u be Element of X holds ((x \ u) \ (z \ y)) <= ((y \ u) \ (z \ x))

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for y,z,u be Element of X holds ((x \ u) \ (z \ y)) <= ((y \ u) \ (z \ x))

      proof

        assume x in ( AtomSet X);

        then

         A1: ex x1 be Element of X st x = x1 & x1 is atom;

        let y,z,u be Element of X;

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

        then (((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x))) = ((((z \ (z \ x)) \ u) \ (z \ y)) \ ((y \ u) \ (z \ x))) by A1;

        then (((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x))) = ((((z \ u) \ (z \ x)) \ (z \ y)) \ ((y \ u) \ (z \ x))) by Th7;

        

        then (((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x))) = ((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) by Th7

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

        then (((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x))) = (((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) \ (((z \ u) \ (z \ y)) \ (y \ u))) by Th1;

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

        hence thesis;

      end;

      assume

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

      now

        let z be Element of X;

        assume

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

        ((x \ ( 0. X)) \ (z \ ( 0. X))) <= ((( 0. X) ` ) \ (z \ x)) by A2;

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

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

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

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

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

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

        hence z = x by A3, Def7;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:28

    

     Th28: for x be Element of X holds x in ( AtomSet X) iff for z be Element of X holds ((z ` ) \ (x ` )) = (x \ z)

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for z be Element of X holds ((z ` ) \ (x ` )) = (x \ z)

      proof

        assume x in ( AtomSet X);

        then

         A1: ex x1 be Element of X st x = x1 & x1 is atom;

        let z be Element of X;

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

        then (z \ (z \ x)) = x by A1;

        then (x \ z) = ((z \ z) \ (z \ x)) by Th7;

        then (x \ z) = ((z \ x) ` ) by Def5;

        hence thesis by Th9;

      end;

      assume

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

      now

        let z be Element of X;

        assume

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

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

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

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

        hence z = x by A3, Def7;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:29

    

     Th29: for x be Element of X holds x in ( AtomSet X) iff ((x ` ) ` ) = x

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies ((x ` ) ` ) = x

      proof

        assume x in ( AtomSet X);

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

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

        hence thesis by Def5;

      end;

      assume

       A1: ((x ` ) ` ) = x;

      now

        let z be Element of X;

        assume

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

        then (((z \ x) \ (x ` )) \ (z \ ( 0. X))) = (x \ z) by A1, Th2;

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

        hence z = x by A2, Def7;

      end;

      then x is atom;

      hence thesis;

    end;

    theorem :: BCIALG_1:30

    

     Th30: for x be Element of X holds x in ( AtomSet X) iff for z be Element of X holds ((z \ x) ` ) = (x \ z)

    proof

      let x be Element of X;

      

       A1: (for z be Element of X holds ((z ` ) \ (x ` )) = (x \ z)) implies for z be Element of X holds ((z \ x) ` ) = (x \ z)

      proof

        assume

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

        let z be Element of X;

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

        hence thesis by Th9;

      end;

      (for z be Element of X holds ((z \ x) ` ) = (x \ z)) implies for z be Element of X holds ((z ` ) \ (x ` )) = (x \ z)

      proof

        assume

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

        let z be Element of X;

        ((z \ x) ` ) = (x \ z) by A3;

        hence thesis by Th9;

      end;

      hence thesis by A1, Th28;

    end;

    theorem :: BCIALG_1:31

    

     Th31: for x be Element of X holds x in ( AtomSet X) iff for z be Element of X holds (((x \ z) ` ) ` ) = (x \ z)

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for z be Element of X holds (((x \ z) ` ) ` ) = (x \ z)

      proof

        assume

         A1: x in ( AtomSet X);

        let z be Element of X;

        

         A2: ((z \ (z \ x)) \ x) = ( 0. X) by Th1;

        ex x1 be Element of X st x = x1 & x1 is atom by A1;

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

        then (((x \ z) ` ) ` ) = ((((z \ z) \ (z \ x)) ` ) ` ) by Th7;

        then (((x \ z) ` ) ` ) = ((((z \ x) ` ) ` ) ` ) by Def5;

        then (((x \ z) ` ) ` ) = ((z \ x) ` ) by Th8;

        hence thesis by A1, Th30;

      end;

      assume for z be Element of X holds (((x \ z) ` ) ` ) = (x \ z);

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

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

      then ((x ` ) ` ) = x by Th2;

      hence thesis by Th29;

    end;

    theorem :: BCIALG_1:32

    for x be Element of X holds x in ( AtomSet X) iff for z,u be Element of X holds (z \ (z \ (x \ u))) = (x \ u)

    proof

      let x be Element of X;

      thus x in ( AtomSet X) implies for z,u be Element of X holds (z \ (z \ (x \ u))) = (x \ u)

      proof

        assume

         A1: x in ( AtomSet X);

        let z,u be Element of X;

        (x \ u) = (((x \ u) ` ) ` ) by A1, Th31

        .= (((z \ z) \ (x \ u)) ` ) by Def5

        .= (((z \ (x \ u)) \ z) ` ) by Th7

        .= (((z \ (x \ u)) ` ) \ (z ` )) by Th9;

        then

         A2: ((x \ u) \ (z \ (z \ (x \ u)))) = ( 0. X) by Th1;

        ((z \ (z \ (x \ u))) \ (x \ u)) = ( 0. X) by Th1;

        hence thesis by A2, Def7;

      end;

      assume for z,u be Element of X holds (z \ (z \ (x \ u))) = (x \ u);

      then (((x \ u) ` ) ` ) = (x \ u);

      hence thesis by Th31;

    end;

    theorem :: BCIALG_1:33

    

     Th33: for a be Element of ( AtomSet X), x be Element of X holds (a \ x) in ( AtomSet X)

    proof

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

      (((a \ x) ` ) ` ) = (a \ x) by Th31;

      hence thesis by Th29;

    end;

    definition

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

      :: original: \

      redefine

      func a \ b -> Element of ( AtomSet X) ;

      coherence by Th33;

    end

    theorem :: BCIALG_1:34

    

     Th34: for x be Element of X holds (x ` ) in ( AtomSet X)

    proof

      let x be Element of X;

      ( 0. X) in ( AtomSet X) by Th23;

      hence thesis by Th33;

    end;

    theorem :: BCIALG_1:35

    

     Th35: for x be Element of X holds ex a be Element of ( AtomSet X) st a <= x

    proof

      let x be Element of X;

      take a = ((x ` ) ` );

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

      hence thesis by Th34;

    end;

    definition

      let X be BCI-algebra;

      :: BCIALG_1:def16

      attr X is generated_by_atom means for x be Element of X holds ex a be Element of ( AtomSet X) st a <= x;

    end

    definition

      let X be BCI-algebra, a be Element of ( AtomSet X);

      :: BCIALG_1:def17

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

      coherence

      proof

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

         A1:

        now

          let y be object;

          assume y in Y;

          then ex x be Element of X st y = x & a <= x;

          hence y in the carrier of X;

        end;

        (a \ a) = ( 0. X) by Def5;

        then a <= a;

        then a in Y;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: BCIALG_1:36

    for X be BCI-algebra holds X is generated_by_atom by Th35;

    theorem :: BCIALG_1:37

    for a,b be Element of ( AtomSet X), x be Element of ( BranchV b) holds (a \ x) = (a \ b)

    proof

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

      (a \ b) in { x1 where x1 be Element of X : x1 is atom };

      then

       A1: ex x1 be Element of X st (a \ b) = x1 & x1 is atom;

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

      then

       A2: ex yy be Element of X st x = yy & b <= yy;

      ((a \ x) \ (a \ b)) = ((a \ (a \ b)) \ x) by Th7;

      then ((a \ x) \ (a \ b)) = (b \ x) by Th24;

      then ((a \ x) \ (a \ b)) = ( 0. X) by A2;

      hence thesis by A1;

    end;

    theorem :: BCIALG_1:38

    

     Th38: for a be Element of ( AtomSet X), x be Element of ( BCK-part X) holds (a \ x) = a

    proof

      let a be Element of ( AtomSet X), x be Element of ( BCK-part X);

      (a \ ( 0. X)) in { x1 where x1 be Element of X : x1 is atom } by Th33;

      then

       A1: ex x1 be Element of X st (a \ ( 0. X)) = x1 & x1 is atom;

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

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

      then

       A2: ((a \ x) \ (a \ ( 0. X))) = (x ` ) by Def5;

      x in { x2 where x2 be Element of X : ( 0. X) <= x2 };

      then ex x2 be Element of X st x = x2 & ( 0. X) <= x2;

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

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

      hence thesis by Th2;

    end;

    

     Lm2: for a be Element of ( AtomSet X), x be Element of ( BranchV a) holds (a \ x) = ( 0. X)

    proof

      let a be Element of ( AtomSet X), x be Element of ( BranchV a);

      x in { x1 where x1 be Element of X : a <= x1 };

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

      hence thesis;

    end;

    theorem :: BCIALG_1:39

    

     Th39: for a,b be Element of ( AtomSet X), x be Element of ( BranchV a), y be Element of ( BranchV b) holds (x \ y) in ( BranchV (a \ b))

    proof

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

      ((a \ b) \ (x \ y)) = ((((a \ b) ` ) ` ) \ (x \ y)) by Th29;

      then ((a \ b) \ (x \ y)) = (((x \ y) ` ) \ ((a \ b) ` )) by Th7;

      then ((a \ b) \ (x \ y)) = (((x ` ) \ (y ` )) \ ((a \ b) ` )) by Th9;

      then ((a \ b) \ (x \ y)) = (((x ` ) \ ((a \ b) ` )) \ (y ` )) by Th7;

      then ((a \ b) \ (x \ y)) = (((((a \ b) ` ) ` ) \ x) \ (y ` )) by Th7;

      then ((a \ b) \ (x \ y)) = (((a \ b) \ x) \ (y ` )) by Th29;

      then ((a \ b) \ (x \ y)) = (((a \ x) \ b) \ (y ` )) by Th7;

      then ((a \ b) \ (x \ y)) = ((b ` ) \ (y ` )) by Lm2;

      then ((a \ b) \ (x \ y)) = ((b \ y) ` ) by Th9;

      then ((a \ b) \ (x \ y)) = (( 0. X) ` ) by Lm2;

      then ((a \ b) \ (x \ y)) = ( 0. X) by Def5;

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

      hence thesis;

    end;

    theorem :: BCIALG_1:40

    for a be Element of ( AtomSet X), x,y be Element of ( BranchV a) holds (x \ y) in ( BCK-part X)

    proof

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

      set b = (a \ a);

      b = ( 0. X) & (x \ y) in ( BranchV b) by Def5, Th39;

      hence thesis;

    end;

    theorem :: BCIALG_1:41

    for a,b be Element of ( AtomSet X), x be Element of ( BranchV a), y be Element of ( BranchV b) st a <> b holds not (x \ y) in ( BCK-part X)

    proof

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

      assume

       A1: a <> b;

      (x \ y) in ( BranchV (a \ b)) by Th39;

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

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

      then ((a \ (x \ y)) \ b) = ( 0. X) by Th7;

      then ((a \ (x \ y)) \ ((a \ (x \ y)) \ b)) = (a \ (x \ y)) by Th2;

      then

       A2: b = (a \ (x \ y)) by Th24;

      assume (x \ y) in ( BCK-part X);

      hence contradiction by A1, A2, Th38;

    end;

    theorem :: BCIALG_1:42

    for a,b be Element of ( AtomSet X) st a <> b holds (( BranchV a) /\ ( BranchV b)) = {}

    proof

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

      assume

       A1: a <> b;

      assume (( BranchV a) /\ ( BranchV b)) <> {} ;

      then

      consider c be object such that

       A2: c in (( BranchV a) /\ ( BranchV b)) by XBOOLE_0:def 1;

      reconsider z2 = c as Element of ( BranchV b) by A2, XBOOLE_0:def 4;

      reconsider z1 = c as Element of ( BranchV a) by A2, XBOOLE_0:def 4;

      (z1 \ z2) in ( BranchV (a \ b)) by Th39;

      then ( 0. X) in { x3 where x3 be Element of X : (a \ b) <= x3 } by Def5;

      then ex x3 be Element of X st ( 0. X) = x3 & (a \ b) <= x3;

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

      then

       A3: (a \ b) = ( 0. X) by Th2;

      b in { xx where xx be Element of X : xx is atom };

      then ex xx be Element of X st b = xx & xx is atom;

      hence contradiction by A1, A3;

    end;

    definition

      let X be BCI-algebra;

      :: BCIALG_1:def18

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

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

      existence

      proof

        take X1 = {( 0. X)};

        

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

        proof

          let x,y be Element of X;

          assume (x \ y) in X1 & y in X1;

          then (x \ y) = ( 0. X) & y = ( 0. X) by TARSKI:def 1;

          then x = ( 0. X) by Th2;

          hence thesis by TARSKI:def 1;

        end;

        now

          let xx be object;

          assume xx in X1;

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

          hence xx in the carrier of X;

        end;

        hence thesis by A1, TARSKI:def 1, TARSKI:def 3;

      end;

    end

    definition

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

      :: BCIALG_1:def19

      attr IT is closed means

      : Def19: for x be Element of IT holds (x ` ) in IT;

    end

    

     Lm3: {( 0. X)} is Ideal of X

    proof

      set X1 = {( 0. X)};

      now

        let xx be object;

        assume xx in X1;

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

        hence xx in the carrier of X;

      end;

      then

       A1: X1 is Subset of X by TARSKI:def 3;

      

       A2: for x,y be Element of X st (x \ y) in {( 0. X)} & y in {( 0. X)} holds x in {( 0. X)}

      proof

        set X1 = {( 0. X)};

        let x,y be Element of X;

        assume (x \ y) in X1 & y in X1;

        then (x \ y) = ( 0. X) & y = ( 0. X) by TARSKI:def 1;

        then x = ( 0. X) by Th2;

        hence thesis by TARSKI:def 1;

      end;

      ( 0. X) in {( 0. X)} by TARSKI:def 1;

      hence thesis by A1, A2, Def18;

    end;

    

     Lm4: for X1 be Ideal of X st X1 = {( 0. X)} holds for x be Element of X1 holds (x ` ) in {( 0. X)}

    proof

      let X1 be Ideal of X;

      assume

       A1: X1 = {( 0. X)};

      let x be Element of X1;

      x = ( 0. X) by A1, TARSKI:def 1;

      then (x ` ) = ( 0. X) by Def5;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let X;

      cluster closed for Ideal of X;

      existence

      proof

        set X1 = {( 0. X)};

        reconsider X1 as Ideal of X by Lm3;

        take X1;

        for x be Element of X1 holds (x ` ) in X1 by Lm4;

        hence thesis;

      end;

    end

    theorem :: BCIALG_1:43

     {( 0. X)} is closed Ideal of X

    proof

      set X1 = {( 0. X)};

      reconsider X1 as Ideal of X by Lm3;

      for x be Element of X1 holds (x ` ) in X1 by Lm4;

      hence thesis by Def19;

    end;

    theorem :: BCIALG_1:44

    the carrier of X is closed Ideal of X

    proof

      

       A1: (for x be Element of X holds (x ` ) in the carrier of X) & for x,y be Element of X st (x \ y) in the carrier of X & y in the carrier of X holds x in the carrier of X;

      the carrier of X is non empty Subset of X & ( 0. X) in the carrier of X by ZFMISC_1:def 1;

      hence thesis by A1, Def18, Def19;

    end;

    theorem :: BCIALG_1:45

    ( BCK-part X) is closed Ideal of X

    proof

      set X1 = ( BCK-part X);

      

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

      proof

        let x,y be Element of X such that

         A2: (x \ y) in X1 and

         A3: y in X1;

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

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

        then

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

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

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

        then (x ` ) = ( 0. X) by Th2;

        then ( 0. X) <= x;

        hence thesis;

      end;

      ( 0. X) in ( BCK-part X) by Th19;

      then

      reconsider X1 as Ideal of X by A1, Def18;

      now

        let x be Element of X1;

        x in X1;

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

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

        then ((x ` ) ` ) = ( 0. X) by Def5;

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

        hence (x ` ) in X1;

      end;

      hence thesis by Def19;

    end;

    

     Lm5: IT is Ideal of X implies for x,y be Element of IT holds { z where z be Element of X : (z \ x) <= y } c= IT

    proof

      assume

       A1: IT is Ideal of X;

      let x,y be Element of IT;

      

       A2: ( 0. X) in IT by A1, Def18;

      let ss be object;

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

      then

       A3: ex z be Element of X st ss = z & (z \ x) <= y;

      then

      reconsider ss as Element of X;

      ((ss \ x) \ y) in IT by A2, A3;

      then (ss \ x) in IT by A1, Def18;

      hence thesis by A1, Def18;

    end;

    theorem :: BCIALG_1:46

    IT is Ideal of X implies for x,y be Element of X st x in IT & y <= x holds y in IT

    proof

      assume

       A1: IT is Ideal of X;

      let x,y be Element of X;

      assume that

       A2: x in IT and

       A3: y <= x;

      (y \ ( 0. X)) <= x by A3, Th2;

      then

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

      ( 0. X) is Element of IT by A1, Def18;

      then { z where z be Element of X : (z \ ( 0. X)) <= x } c= IT by A1, A2, Lm5;

      hence thesis by A4;

    end;

    begin

    definition

      let IT be BCI-algebra;

      :: BCIALG_1:def20

      attr IT is associative means

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

      :: BCIALG_1:def21

      attr IT is quasi-associative means for x be Element of IT holds ((x ` ) ` ) = (x ` );

      :: BCIALG_1:def22

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

      :: BCIALG_1:def23

      attr IT is weakly-positive-implicative means

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

      :: BCIALG_1:def24

      attr IT is implicative means

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

      :: BCIALG_1:def25

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

      :: BCIALG_1:def26

      attr IT is p-Semisimple means

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

      :: BCIALG_1:def27

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

    end

    registration

      cluster BCI-EXAMPLE -> implicative positive-implicative p-Semisimple associative weakly-implicative weakly-positive-implicative;

      coherence by STRUCT_0:def 10;

    end

    registration

      cluster implicative positive-implicative p-Semisimple associative weakly-implicative weakly-positive-implicative for BCI-algebra;

      existence

      proof

        take BCI-EXAMPLE ;

        thus thesis;

      end;

    end

    

     Lm6: (for x,y be Element of X holds (y \ x) = (x \ y)) implies X is associative

    proof

      assume

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

      let x,y,z be Element of X;

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

      .= ((y \ x) \ z) by Th7;

      hence thesis by A1;

    end;

    

     Lm7: (for x holds (x ` ) = x) implies for x, y holds (x \ y) = (y \ x)

    proof

      assume

       A1: for x holds (x ` ) = x;

      let x, y;

      

       A2: ((y \ x) \ (x \ y)) = (((y ` ) \ x) \ (x \ y)) by A1

      .= (((y ` ) \ (x ` )) \ (x \ y)) by A1

      .= ( 0. X) by Th1;

      ((x \ y) \ (y \ x)) = (((x ` ) \ y) \ (y \ x)) by A1

      .= (((x ` ) \ (y ` )) \ (y \ x)) by A1

      .= ( 0. X) by Th1;

      hence thesis by A2, Def7;

    end;

    theorem :: BCIALG_1:47

    

     Th47: X is associative iff for x be Element of X holds (x ` ) = x

    proof

      thus X is associative implies for x be Element of X holds (x ` ) = x

      proof

        assume

         A1: X is associative;

        let x be Element of X;

        

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

        .= (x \ x) by Th2

        .= ( 0. X) by Def5;

        ((x ` ) \ x) = ((x \ x) ` ) by A1

        .= (( 0. X) ` ) by Def5

        .= ( 0. X) by Def5;

        hence thesis by A2, Def7;

      end;

      assume for x be Element of X holds (x ` ) = x;

      then for x, y holds (x \ y) = (y \ x) by Lm7;

      hence thesis by Lm6;

    end;

    theorem :: BCIALG_1:48

    

     Th48: (for x,y be Element of X holds (y \ x) = (x \ y)) iff X is associative

    proof

      thus (for x,y be Element of X holds (y \ x) = (x \ y)) implies X is associative by Lm6;

      assume X is associative;

      then for x be Element of X holds (x ` ) = x by Th47;

      hence thesis by Lm7;

    end;

    theorem :: BCIALG_1:49

    

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

    proof

      let X be non empty BCIStr_0;

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

      proof

        assume

         A1: X is associative BCI-algebra;

        let x,y,z be Element of X;

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

        then ((z \ y) \ ((y \ x) \ (z \ x))) = (((z \ y) \ (z \ x)) \ (y \ x)) by A1, Th7;

        then ((z \ y) \ ((y \ x) \ (z \ x))) = (((z \ y) \ (z \ x)) \ (x \ y)) by A1, Th48;

        then

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

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

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

        hence thesis by A1, A2, Def7, Th2;

      end;

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

      proof

        assume

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

        

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

        proof

          let x,y be Element of X;

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

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

          hence thesis by A3;

        end;

        

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

        proof

          let a be Element of X;

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

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

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

          then (a \ a) = (( 0. X) ` ) by A3;

          hence thesis by A3;

        end;

        

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

        proof

          let x,y,z be Element of X;

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

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

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

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

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

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

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

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

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

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

        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 that

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

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

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

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

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

          

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

          .= x by A3, A7;

          hence thesis;

        end;

        then

         A8: X is being_BCI-4;

        X is being_I by A5;

        then

        reconsider Y = X as BCI-algebra by A6, A8, Th1;

        Y is associative by A4, Th48;

        hence thesis;

      end;

    end;

    theorem :: BCIALG_1:50

    

     Th50: for X be non empty BCIStr_0 holds (X is associative BCI-algebra iff for x,y,z be Element of X holds ((x \ y) \ (x \ z)) = (z \ y) & (x ` ) = x)

    proof

      let X be non empty BCIStr_0;

      thus X is associative BCI-algebra implies for x,y,z be Element of X holds ((x \ y) \ (x \ z)) = (z \ y) & (x ` ) = x

      proof

        assume

         A1: X is associative BCI-algebra;

        let x,y,z be Element of X;

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

        then

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

        (x \ ( 0. X)) = x by A1, Th49;

        hence thesis by A1, A2, Th48;

      end;

      assume

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

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

      proof

        

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

        proof

          let x,y be Element of X;

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

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

          hence thesis by A3;

        end;

        let x,y,z be Element of X;

        

         A5: (x ` ) = x by A3;

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

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

        hence thesis by A4, A5;

      end;

      hence thesis by Th49;

    end;

    theorem :: BCIALG_1:51

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

    proof

      let X be non empty BCIStr_0;

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

      proof

        assume

         A1: X is associative BCI-algebra;

        let x,y,z be Element of X;

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

        then ((x \ y) \ (z \ x)) = (z \ y) by A1, Th48;

        then ((x \ y) \ (x \ z)) = (z \ y) by A1, Th48;

        hence thesis by A1, Th48, Th49;

      end;

      assume

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

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

      proof

        let x,y,z be Element of X;

        

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

        proof

          let x,y be Element of X;

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

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

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

          then

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

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

          hence thesis by A2, A4;

        end;

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

        hence thesis by A3;

      end;

      hence thesis by Th50;

    end;

    begin

    theorem :: BCIALG_1:52

    X is p-Semisimple iff for x be Element of X holds x is atom

    proof

      thus X is p-Semisimple implies for x be Element of X holds x is atom

      proof

        assume

         A1: X is p-Semisimple;

        let x be Element of X;

        now

          let z be Element of X;

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

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

          hence z = x by Th2;

        end;

        hence thesis;

      end;

      assume

       A2: for x be Element of X holds x is atom;

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

      proof

        let x,y be Element of X;

        y is atom & ((x \ (x \ y)) \ y) = ( 0. X) by A2, Th1;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_1:53

    X is p-Semisimple implies ( BCK-part X) = {( 0. X)}

    proof

      assume

       A1: X is p-Semisimple;

      thus ( BCK-part X) c= {( 0. X)}

      proof

        let x be object;

        assume

         A2: x in ( BCK-part X);

        then

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

        reconsider x as Element of X by A2;

        ((x ` ) ` ) = x by A1;

        then (( 0. X) ` ) = x by A3;

        then x = ( 0. X) by Def5;

        hence thesis by TARSKI:def 1;

      end;

      thus {( 0. X)} c= ( BCK-part X)

      proof

        let x be object;

        assume

         A4: x in {( 0. X)};

        then

        reconsider x as Element of X by TARSKI:def 1;

        x = ( 0. X) by A4, TARSKI:def 1;

        then (x ` ) = ( 0. X) by Def5;

        then ( 0. X) <= x;

        hence thesis;

      end;

    end;

    

     Lm8: (for x, y holds (y \ (y \ x)) = x) iff for x, y, z holds ((z \ y) \ (z \ x)) = (x \ y)

    proof

      thus (for x, y holds (y \ (y \ x)) = x) implies for x, y, z holds ((z \ y) \ (z \ x)) = (x \ y)

      proof

        assume

         A1: for x, y holds (y \ (y \ x)) = x;

        let x, y, z;

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

        hence thesis by A1;

      end;

      assume

       A2: for x, y, z holds ((z \ y) \ (z \ x)) = (x \ y);

      let x, y;

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

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

      hence thesis by Th2;

    end;

    theorem :: BCIALG_1:54

    

     Th54: X is p-Semisimple iff for x be Element of X holds ((x ` ) ` ) = x

    proof

      (for x be Element of X holds ((x ` ) ` ) = x) implies X is p-Semisimple

      proof

        assume

         A1: for x be Element of X holds ((x ` ) ` ) = x;

        now

          let x,y be Element of X;

          

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

          (y \ (x \ (x \ y))) = (((y \ (x \ (x \ y))) ` ) ` ) by A1

          .= (((y ` ) \ ((x \ (x \ y)) ` )) ` ) by Th9

          .= (( 0. X) \ (((( 0. X) \ y) \ ((x \ (x \ y)) ` )) \ ( 0. X))) by Th2

          .= (( 0. X) \ (((( 0. X) \ y) \ ((x \ (x \ y)) ` )) \ ((x \ (x \ y)) \ y))) by Th1

          .= (( 0. X) \ ( 0. X)) by Th1

          .= ( 0. X) by Def5;

          hence (x \ (x \ y)) = y by A2, Def7;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_1:55

    X is p-Semisimple iff for x, y holds (y \ (y \ x)) = x;

    theorem :: BCIALG_1:56

    

     Th56: X is p-Semisimple iff for x, y, z holds ((z \ y) \ (z \ x)) = (x \ y)

    proof

      X is p-Semisimple iff for x, y holds (y \ (y \ x)) = x;

      hence thesis by Lm8;

    end;

    theorem :: BCIALG_1:57

    

     Th57: X is p-Semisimple iff for x, y, z holds (x \ (z \ y)) = (y \ (z \ x))

    proof

      thus X is p-Semisimple implies for x, y, z holds (x \ (z \ y)) = (y \ (z \ x))

      proof

        assume

         A1: X is p-Semisimple;

        let x, y, z;

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

        then

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

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

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

        hence thesis by A2, Def7;

      end;

      assume

       A3: for x, y, z holds (x \ (z \ y)) = (y \ (z \ x));

      for x holds ((x ` ) ` ) = x

      proof

        let x;

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

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

        hence thesis by Th2;

      end;

      hence thesis by Th54;

    end;

    

     Lm9: X is p-Semisimple implies for x, y, z, u holds ((x \ u) \ (z \ y)) = ((y \ u) \ (z \ x)) & ((x \ u) \ (z \ y)) = ((x \ z) \ (u \ y))

    proof

      assume

       A1: X is p-Semisimple;

      let x, y, z, u;

      

       A2: ((x \ u) \ (z \ y)) = ((x \ (z \ y)) \ u) by Th7

      .= ((y \ (z \ x)) \ u) by A1, Th57;

      ((x \ u) \ (z \ y)) = (y \ (z \ (x \ u))) by A1, Th57

      .= (y \ (u \ (x \ z))) by A1, Th57

      .= ((x \ z) \ (u \ y)) by A1, Th57;

      hence thesis by A2, Th7;

    end;

    

     Lm10: X is p-Semisimple implies for x, y holds ((y ` ) \ (( 0. X) \ x)) = (x \ y)

    proof

      assume

       A1: X is p-Semisimple;

      let x, y;

      ((y ` ) \ (( 0. X) \ x)) = ((x \ y) \ (( 0. X) \ ( 0. X))) by A1, Lm9

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

      hence thesis by Th2;

    end;

    

     Lm11: X is p-Semisimple implies for x, y, z holds ((x \ y) \ (z \ y)) = (x \ z)

    proof

      assume

       A1: X is p-Semisimple;

      let x, y, z;

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

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

      hence thesis by Th2;

    end;

    

     Lm12: X is p-Semisimple implies for x, y, z st (x \ y) = (x \ z) holds y = z

    proof

      assume

       A1: X is p-Semisimple;

      let x, y, z;

      assume

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

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

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

      then ((x \ z) \ (x \ y)) = (y \ z) by Th2;

      then

       A3: ( 0. X) = (y \ z) by A2, Def5;

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

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

      then ((x \ y) \ (x \ z)) = (z \ y) by Th2;

      then ( 0. X) = (z \ y) by A2, Def5;

      hence thesis by A3, Def7;

    end;

    

     Lm13: X is p-Semisimple implies for x, y, z holds (x \ (y \ z)) = ((z \ y) \ (x ` ))

    proof

      assume

       A1: X is p-Semisimple;

      let x, y, z;

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

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

      hence thesis by A1, Lm9;

    end;

    

     Lm14: X is p-Semisimple implies for x, y, z st (y \ x) = (z \ x) holds y = z

    proof

      assume

       A1: X is p-Semisimple;

      let x, y, z;

      assume

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

      

       A3: (z \ y) = ((z \ x) \ (y \ x)) by A1, Lm11

      .= ( 0. X) by A2, Def5;

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

      .= ( 0. X) by A2, Def5;

      hence thesis by A3, Def7;

    end;

    theorem :: BCIALG_1:58

    X is p-Semisimple iff for x, y, z, u holds ((x \ u) \ (z \ y)) = ((y \ u) \ (z \ x))

    proof

      thus X is p-Semisimple implies for x, y, z, u holds ((x \ u) \ (z \ y)) = ((y \ u) \ (z \ x)) by Lm9;

      thus (for x, y, z, u holds ((x \ u) \ (z \ y)) = ((y \ u) \ (z \ x))) implies X is p-Semisimple

      proof

        assume

         A1: for x, y, z, u holds ((x \ u) \ (z \ y)) = ((y \ u) \ (z \ x));

        for x, y, z holds (x \ (z \ y)) = (y \ (z \ x))

        proof

          let x, y, z;

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

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

          hence thesis by Th2;

        end;

        hence thesis by Th57;

      end;

    end;

    theorem :: BCIALG_1:59

    

     Th59: X is p-Semisimple iff for x, z holds ((z ` ) \ (x ` )) = (x \ z)

    proof

      thus X is p-Semisimple implies for x, z holds ((z ` ) \ (x ` )) = (x \ z) by Lm10;

      assume

       A1: for x, z holds ((z ` ) \ (x ` )) = (x \ z);

      for x holds ((x ` ) ` ) = x

      proof

        let x;

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

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

        hence thesis by Th2;

      end;

      hence thesis by Th54;

    end;

    theorem :: BCIALG_1:60

    X is p-Semisimple iff for x, z holds (((x \ z) ` ) ` ) = (x \ z)

    proof

      thus X is p-Semisimple implies for x, z holds (((x \ z) ` ) ` ) = (x \ z);

      assume

       A1: for x, z holds (((x \ z) ` ) ` ) = (x \ z);

      now

        let x;

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

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

        hence ((x ` ) ` ) = x by Th2;

      end;

      hence thesis by Th54;

    end;

    theorem :: BCIALG_1:61

    X is p-Semisimple iff for x, u, z holds (z \ (z \ (x \ u))) = (x \ u)

    proof

      thus X is p-Semisimple implies for x, u, z holds (z \ (z \ (x \ u))) = (x \ u);

      assume

       A1: for x, u, z holds (z \ (z \ (x \ u))) = (x \ u);

      now

        let x;

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

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

        hence ((x ` ) ` ) = x by Th2;

      end;

      hence thesis by Th54;

    end;

    theorem :: BCIALG_1:62

    

     Th62: X is p-Semisimple iff for x st (x ` ) = ( 0. X) holds x = ( 0. X)

    proof

      thus X is p-Semisimple implies for x st (x ` ) = ( 0. X) holds x = ( 0. X)

      proof

        assume

         A1: X is p-Semisimple;

        let x;

        assume (x ` ) = ( 0. X);

        then ((x ` ) ` ) = ( 0. X) by Def5;

        hence thesis by A1;

      end;

      assume

       A2: for x st (x ` ) = ( 0. X) holds x = ( 0. X);

      for x holds ((x ` ) ` ) = x

      proof

        let x;

        ((x \ ((x ` ) ` )) ` ) = ((x ` ) \ (((x ` ) ` ) ` )) by Th9

        .= ((x ` ) \ (x ` )) by Th8

        .= ( 0. X) by Def5;

        then

         A3: (x \ ((x ` ) ` )) = ( 0. X) by A2;

        (((x ` ) ` ) \ x) = ( 0. X) by Th1;

        hence thesis by A3, Def7;

      end;

      hence thesis by Th54;

    end;

    theorem :: BCIALG_1:63

    

     Th63: X is p-Semisimple iff for x, y holds (x \ (y ` )) = (y \ (x ` ))

    proof

      thus X is p-Semisimple implies for x, y holds (x \ (y ` )) = (y \ (x ` )) by Th57;

      assume

       A1: for x, y holds (x \ (y ` )) = (y \ (x ` ));

      now

        let x;

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

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

        hence x = ((x ` ) ` ) by Th2;

      end;

      hence thesis by Th54;

    end;

    theorem :: BCIALG_1:64

    X is p-Semisimple iff for x, y, z, u holds ((x \ y) \ (z \ u)) = ((x \ z) \ (y \ u))

    proof

      thus X is p-Semisimple implies for x, y, z, u holds ((x \ y) \ (z \ u)) = ((x \ z) \ (y \ u)) by Lm9;

      assume

       A1: for x, y, z, u holds ((x \ y) \ (z \ u)) = ((x \ z) \ (y \ u));

      for x, z holds ((z ` ) \ (x ` )) = (x \ z)

      proof

        let x, z;

        ((z \ x) ` ) = ((x \ x) \ (z \ x)) by Def5;

        then ((z \ x) ` ) = ((x \ z) \ (x \ x)) by A1;

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

        then ((z \ x) ` ) = (x \ z) by Th2;

        hence thesis by Th9;

      end;

      hence thesis by Th59;

    end;

    theorem :: BCIALG_1:65

    X is p-Semisimple iff for x, y, z holds ((x \ y) \ (z \ y)) = (x \ z)

    proof

      thus X is p-Semisimple implies for x, y, z holds ((x \ y) \ (z \ y)) = (x \ z) by Lm11;

      assume

       A1: for x, y, z holds ((x \ y) \ (z \ y)) = (x \ z);

      for x, z holds ((z ` ) \ (x ` )) = (x \ z)

      proof

        let x, z;

        ((z \ x) ` ) = ((x \ x) \ (z \ x)) by Def5;

        then ((z \ x) ` ) = (x \ z) by A1;

        hence thesis by Th9;

      end;

      hence thesis by Th59;

    end;

    theorem :: BCIALG_1:66

    X is p-Semisimple iff for x, y, z holds (x \ (y \ z)) = ((z \ y) \ (x ` ))

    proof

      thus X is p-Semisimple implies for x, y, z holds (x \ (y \ z)) = ((z \ y) \ (x ` )) by Lm13;

      assume

       A1: for x, y, z holds (x \ (y \ z)) = ((z \ y) \ (x ` ));

      for x, y holds (x \ (y ` )) = (y \ (x ` ))

      proof

        let x, y;

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

        hence thesis by Th2;

      end;

      hence thesis by Th63;

    end;

    theorem :: BCIALG_1:67

    X is p-Semisimple iff for x, y, z st (y \ x) = (z \ x) holds y = z

    proof

      thus X is p-Semisimple implies for x, y, z st (y \ x) = (z \ x) holds y = z by Lm14;

      assume

       A1: for x, y, z st (y \ x) = (z \ x) holds y = z;

      for x, y holds (x \ (x \ y)) = y

      proof

        let x, y;

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

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

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_1:68

    X is p-Semisimple iff for x, y, z st (x \ y) = (x \ z) holds y = z

    proof

      thus X is p-Semisimple implies for x, y, z st (x \ y) = (x \ z) holds y = z by Lm12;

      assume

       A1: for x, y, z st (x \ y) = (x \ z) holds y = z;

      for x st (x ` ) = ( 0. X) holds x = ( 0. X)

      proof

        let x;

        assume (x ` ) = ( 0. X);

        then (x ` ) = (( 0. X) ` ) by Def5;

        hence thesis by A1;

      end;

      hence thesis by Th62;

    end;

    theorem :: BCIALG_1:69

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

    proof

      let X be non empty BCIStr_0;

      thus X is p-Semisimple BCI-algebra implies for x,y,z be Element of X holds ((x \ y) \ (x \ z)) = (z \ y) & (x \ ( 0. X)) = x by Th2, Th56;

      assume

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

       A2:

      now

        let x,y,z be Element of X;

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

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

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

        .= (( 0. X) ` ) by A1;

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

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

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

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

        .= (( 0. X) ` ) by A1;

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

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

        proof

          let x,y be Element of X;

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

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

          hence thesis by A1;

        end;

      end;

      now

        let x,y be Element of X;

        assume that

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

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

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

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

        hence x = y by A1;

      end;

      then

       A4: X is being_BCI-4;

      now

        let x be Element of X;

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

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

        .= (( 0. X) ` ) by A1;

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

      end;

      then X is being_I;

      hence thesis by A4, A2, Def26, Th1;

    end;

    theorem :: BCIALG_1:70

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

    proof

      let X be non empty BCIStr_0;

      thus X is p-Semisimple BCI-algebra implies (X is being_I & for x,y,z be Element of X holds (x \ (y \ z)) = (z \ (y \ x)) & (x \ ( 0. X)) = x) by Th2, Th57;

      assume that

       A1: X is being_I and

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

       A3:

      now

        let x,y,z be Element of X;

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

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

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

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

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

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

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

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

        .= (y \ y) by A2;

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

        thus 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 \ x)) by A2;

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

          hence thesis by A2;

        end;

      end;

      now

        let x,y be Element of X;

        assume that

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

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

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

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

        hence x = y by A2;

      end;

      then X is being_BCI-4;

      hence thesis by A1, A3, Def26, Th1;

    end;

    begin

    

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

    proof

      assume

       A1: for x be Element of X holds (x ` ) <= x;

      let x,y be Element of X;

      ((y \ x) ` ) = ((((y \ x) ` ) ` ) ` ) by Th8

      .= ((((y ` ) \ (x ` )) ` ) ` ) by Th9

      .= ((((y ` ) ` ) \ ((x ` ) ` )) ` ) by Th9

      .= (((((x ` ) ` ) ` ) \ (y ` )) ` ) by Th7

      .= (((x ` ) \ (y ` )) ` ) by Th8

      .= (((x \ y) ` ) ` ) by Th9;

      then ((y \ x) ` ) <= ((x \ y) ` ) by A1;

      then

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

      ((x \ y) ` ) = ((((x \ y) ` ) ` ) ` ) by Th8

      .= ((((x ` ) \ (y ` )) ` ) ` ) by Th9

      .= ((((x ` ) ` ) \ ((y ` ) ` )) ` ) by Th9

      .= (((((y ` ) ` ) ` ) \ (x ` )) ` ) by Th7

      .= (((y ` ) \ (x ` )) ` ) by Th8

      .= (((y \ x) ` ) ` ) by Th9;

      then ((x \ y) ` ) <= ((y \ x) ` ) by A1;

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

      hence thesis by A2, Def7;

    end;

    

     Lm16: (for x,y be Element of X holds ((x \ y) ` ) = ((y \ x) ` )) implies for x,y be Element of X holds ((x ` ) \ y) = ((x \ y) ` )

    proof

      assume

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

      let x,y be Element of X;

      

      thus ((x \ y) ` ) = ((x ` ) \ (y ` )) by Th9

      .= (((y ` ) ` ) \ x) by Th7

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

      .= ((y ` ) \ x) by Th2

      .= ((x ` ) \ y) by Th7;

    end;

    

     Lm17: (for x,y be Element of X holds ((x ` ) \ y) = ((x \ y) ` )) implies for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X)

    proof

      assume

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

      let x,y be Element of X;

      (((x \ y) \ (y \ x)) ` ) = (((x \ y) ` ) \ (y \ x)) by A1

      .= (((x ` ) \ (y ` )) \ (y \ x)) by Th9

      .= ((((y ` ) ` ) \ x) \ (y \ x)) by Th7

      .= ((((y ` ) \ x) ` ) \ (y \ x)) by A1

      .= ((((y \ x) ` ) ` ) \ (y \ x)) by A1

      .= ( 0. X) by Th1;

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

      hence thesis;

    end;

    

     Lm18: (for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X)) implies X is quasi-associative

    proof

      assume

       A1: for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X);

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

      proof

        let x be Element of X;

        (x \ (x ` )) = ((x \ ( 0. X)) \ (x ` )) by Th2;

        then (x \ (x ` )) in { x2 where x2 be Element of X : ( 0. X) <= x2 } by A1;

        then ex x2 be Element of X st (x \ (x ` )) = x2 & ( 0. X) <= x2;

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

        then

         A2: ((x ` ) \ ((x ` ) ` )) = ( 0. X) by Th9;

        ((x ` ) \ x) = ((x ` ) \ (x \ ( 0. X))) by Th2;

        then ((x ` ) \ x) in { x1 where x1 be Element of X : ( 0. X) <= x1 } by A1;

        then ex x1 be Element of X st ((x ` ) \ x) = x1 & ( 0. X) <= x1;

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

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

        hence thesis by A2, Def7;

      end;

      hence thesis;

    end;

    

     Lm19: (for x be Element of X holds (x ` ) <= x) iff for x,y,z be Element of X holds ((x \ y) \ z) <= (x \ (y \ z))

    proof

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

      proof

        assume

         A1: for x be Element of X holds (x ` ) <= x;

        let x,y,z be Element of X;

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

        then

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

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

        .= (((x \ (x \ (y \ z))) \ y) \ z) by Th7;

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

        then

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

        (z ` ) <= z by A1;

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

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

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

        hence thesis;

      end;

      assume

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

      let x be Element of X;

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

      then (x ` ) <= ((x ` ) ` ) by Def5;

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

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

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

      hence thesis;

    end;

    theorem :: BCIALG_1:71

    

     Th71: X is quasi-associative iff for x be Element of X holds (x ` ) <= x

    proof

      thus X is quasi-associative implies for x be Element of X holds (x ` ) <= x

      proof

        assume

         A1: X is quasi-associative;

        let x be Element of X;

        (((x ` ) ` ) \ x) = ( 0. X) by Th1;

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

        hence thesis;

      end;

      assume for x be Element of X holds (x ` ) <= x;

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

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

      then for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X) by Lm17;

      hence thesis by Lm18;

    end;

    theorem :: BCIALG_1:72

    

     Th72: X is quasi-associative iff for x,y be Element of X holds ((x \ y) ` ) = ((y \ x) ` )

    proof

      thus X is quasi-associative implies for x,y be Element of X holds ((x \ y) ` ) = ((y \ x) ` )

      proof

        assume X is quasi-associative;

        then for x be Element of X holds (x ` ) <= x by Th71;

        hence thesis by Lm15;

      end;

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

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

      then for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X) by Lm17;

      hence thesis by Lm18;

    end;

    theorem :: BCIALG_1:73

    

     Th73: X is quasi-associative iff for x,y be Element of X holds ((x ` ) \ y) = ((x \ y) ` )

    proof

      thus X is quasi-associative implies for x,y be Element of X holds ((x ` ) \ y) = ((x \ y) ` )

      proof

        assume X is quasi-associative;

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

        hence thesis by Lm16;

      end;

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

      then for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X) by Lm17;

      hence thesis by Lm18;

    end;

    theorem :: BCIALG_1:74

    X is quasi-associative iff for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X)

    proof

      thus X is quasi-associative implies for x,y be Element of X holds ((x \ y) \ (y \ x)) in ( BCK-part X)

      proof

        assume X is quasi-associative;

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

        hence thesis by Lm17;

      end;

      thus thesis by Lm18;

    end;

    theorem :: BCIALG_1:75

    X is quasi-associative iff for x,y,z be Element of X holds ((x \ y) \ z) <= (x \ (y \ z))

    proof

      thus X is quasi-associative implies for x,y,z be Element of X holds ((x \ y) \ z) <= (x \ (y \ z))

      proof

        assume X is quasi-associative;

        then for x be Element of X holds (x ` ) <= x by Th71;

        hence thesis by Lm19;

      end;

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

      then for x be Element of X holds (x ` ) <= x by Lm19;

      hence thesis by Th71;

    end;

    begin

    theorem :: BCIALG_1:76

    

     Th76: X is alternative implies (x ` ) = x & (x \ (x \ y)) = y & ((x \ y) \ y) = x

    proof

      assume

       A1: X is alternative;

      then (x \ (x \ x)) = ((x \ x) \ x);

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

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

      hence (x ` ) = x by Th2;

      (y \ (y \ y)) = ((y \ y) \ y) by A1;

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

      then (y \ ( 0. X)) = (y ` ) by Def5;

      then

       A2: y = (y ` ) by Th2;

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

      hence (x \ (x \ y)) = y by A2, Def5;

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

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

      hence thesis by Th2;

    end;

    theorem :: BCIALG_1:77

    X is alternative & (x \ a) = (x \ b) implies a = b

    proof

      assume that

       A1: X is alternative and

       A2: (x \ a) = (x \ b);

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

      then ((x \ x) \ a) = ((x \ x) \ b) by A1;

      then (a ` ) = ((x \ x) \ b) by Def5;

      then (a ` ) = (b ` ) by Def5;

      then a = (b ` ) by A1, Th76;

      hence thesis by A1, Th76;

    end;

    theorem :: BCIALG_1:78

    X is alternative & (a \ x) = (b \ x) implies a = b

    proof

      assume that

       A1: X is alternative and

       A2: (a \ x) = (b \ x);

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

      then (a \ (x \ x)) = (b \ (x \ x)) by A1;

      then (a \ ( 0. X)) = (b \ (x \ x)) by Def5;

      then (a \ ( 0. X)) = (b \ ( 0. X)) by Def5;

      then a = (b \ ( 0. X)) by Th2;

      hence thesis by Th2;

    end;

    theorem :: BCIALG_1:79

    X is alternative & (x \ y) = ( 0. X) implies x = y

    proof

      assume that

       A1: X is alternative and

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

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

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

      then (y ` ) = x by Def5;

      hence thesis by A1, Th76;

    end;

    theorem :: BCIALG_1:80

    X is alternative & ((x \ a) \ b) = ( 0. X) implies a = (x \ b) & b = (x \ a)

    proof

      assume that

       A1: X is alternative and

       A2: ((x \ a) \ b) = ( 0. X);

      ((x \ a) \ (b \ b)) = (b ` ) by A1, A2;

      then ((x \ a) \ ( 0. X)) = (b ` ) by Def5;

      then (x \ a) = (b ` ) by Th2;

      then (x \ (x \ a)) = (x \ b) by A1, Th76;

      then ((x \ x) \ a) = (x \ b) by A1;

      then (a ` ) = (x \ b) by Def5;

      then a = (x \ b) by A1, Th76;

      hence thesis by A1, Th76;

    end;

    

     Lm20: X is alternative iff X is associative

    proof

      thus X is alternative implies X is associative

      proof

        assume

         A1: X is alternative;

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

        proof

          let x,y,z be Element of X;

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

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

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

          then (((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z ` ) \ (y \ z)) \ y)) = ( 0. X) by A1, Th76;

          then (((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z ` ) \ (y \ z)) \ (y ` ))) = ( 0. X) by A1, Th76;

          then

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

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

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

          then (((x \ y) \ z) \ (x \ (y \ z))) = ((((x \ x) \ (y \ z)) \ y) \ z) by A1;

          then (((x \ y) \ z) \ (x \ (y \ z))) = ((((y \ z) ` ) \ y) \ z) by Def5;

          then (((x \ y) \ z) \ (x \ (y \ z))) = (((y \ z) \ y) \ z) by A1, Th76;

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

          then (((x \ y) \ z) \ (x \ (y \ z))) = ((z ` ) \ z) by Def5;

          then

           A3: (((x \ y) \ z) \ (x \ (y \ z))) = ( 0. X) by A1, Th76;

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

          .= ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) by Th7;

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

          hence thesis by A3, Def7;

        end;

        hence thesis;

      end;

      assume X is associative;

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

      hence thesis;

    end;

    

     Lm21: X is alternative implies X is implicative by Th76;

    registration

      cluster alternative -> associative for BCI-algebra;

      coherence by Lm20;

      cluster associative -> alternative for BCI-algebra;

      coherence ;

      cluster alternative -> implicative for BCI-algebra;

      coherence by Lm21;

    end

    theorem :: BCIALG_1:81

    X is alternative implies ((x \ (x \ y)) \ (y \ x)) = x

    proof

      assume

       A1: X is alternative;

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

      hence thesis by A1, Th76;

    end;

    theorem :: BCIALG_1:82

    X is alternative implies (y \ (y \ (x \ (x \ y)))) = y

    proof

      assume X is alternative;

      

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

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

      .= y by Th2;

      hence thesis;

    end;

    begin

    

     Lm22: X is associative implies X is weakly-positive-implicative

    proof

      assume

       A1: X is associative;

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

      proof

        let x,y,z be Element of X;

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

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

        then ((x \ y) \ z) = ((x \ (z \ z)) \ (y \ z)) by Def5;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    

     Lm23: X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative BCI-algebra

    proof

      assume

       A1: X is p-Semisimple BCI-algebra;

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

      proof

        let x,y,z be Element of X;

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

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

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

        hence thesis by Th2;

      end;

      hence thesis by Def23;

    end;

    registration

      cluster associative -> weakly-positive-implicative for BCI-algebra;

      coherence by Lm22;

      cluster p-Semisimple -> weakly-positive-implicative for BCI-algebra;

      coherence by Lm23;

    end

    theorem :: BCIALG_1:83

    for X be non empty BCIStr_0 holds (X is implicative 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 \ x)) = (y \ (y \ x)))

    proof

      let X be non empty BCIStr_0;

      thus X is implicative BCI-algebra implies 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 \ x)) = (y \ (y \ x)) by Def24, Th1, Th2;

      thus (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 \ x)) = (y \ (y \ x))) implies X is implicative 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 \ x)) = (y \ (y \ x));

         A2:

        now

          let x,y,z be Element of X;

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

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

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

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

        end;

        now

          let x,y be Element of X;

          assume that

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

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

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

          .= ((y \ (y \ x)) \ (x \ y)) by A1, A3

          .= (y \ ( 0. X)) by A1, A3, A4;

          hence x = y by A1;

        end;

        then

         A5: X is being_BCI-4;

        now

          let x be Element of X;

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

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

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

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

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

        end;

        then X is being_I;

        hence thesis by A1, A5, A2, Def24, Th1;

      end;

    end;

    theorem :: BCIALG_1:84

    

     Th84: X is weakly-positive-implicative iff for x,y be Element of X holds (x \ y) = (((x \ y) \ y) \ (y ` ))

    proof

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

      proof

        assume

         A1: X is weakly-positive-implicative;

        let x,y be Element of X;

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

        hence thesis by Th2;

      end;

      assume

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

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

      proof

        let x,y,z be Element of X;

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

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

        then

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

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

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

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

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

        then

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

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

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

        .= (((((x \ z) \ z) \ (z ` )) \ (((x \ z) \ z) \ (y \ z))) \ y) by Th7

        .= (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z ` )) \ y) by Th7;

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

        hence thesis by A3, Def7;

      end;

      hence thesis;

    end;

    

     Lm24: X is weakly-positive-implicative implies ((x \ (x \ y)) \ (y \ x)) = (((y \ (y \ x)) \ (y \ x)) \ (x \ y))

    proof

      assume

       A1: X is weakly-positive-implicative;

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

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

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

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

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

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

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

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

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

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

      then

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

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

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

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

      hence thesis by A2, Def7;

    end;

    

     Lm25: X is positive-implicative iff X is weakly-positive-implicative

    proof

      thus X is positive-implicative implies X is weakly-positive-implicative

      proof

        assume

         A1: X is positive-implicative;

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

        proof

          let x,y be Element of X;

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

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

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

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

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

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

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

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

          hence thesis by Def5;

        end;

        hence thesis by Th84;

      end;

      assume

       A2: X is weakly-positive-implicative;

      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;

        

         A3: ((x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x))) = ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) by A2, Lm24;

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

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

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

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

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

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

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

        then

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

        (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) ` ))) = (((((y \ (y \ x)) \ (y \ x)) \ ((y \ x) ` )) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) ` ))) by A2, Th84

        .= ( 0. X) by Th1;

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

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

        then

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

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

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

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

        then

         A6: ((x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x))) = ( 0. X) by A3, Th2;

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

        hence thesis by A6, Def7;

      end;

      hence thesis;

    end;

    registration

      cluster positive-implicative -> weakly-positive-implicative for BCI-algebra;

      coherence by Lm25;

      cluster alternative -> weakly-positive-implicative for BCI-algebra;

      coherence ;

    end

    theorem :: BCIALG_1:85

    X is weakly-positive-implicative BCI-algebra implies for x,y be Element of X holds ((x \ (x \ y)) \ (y \ x)) = (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) by Lm24;

    theorem :: BCIALG_1:86

    for X be non empty BCIStr_0 holds (X is positive-implicative 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 \ y) = (((x \ y) \ y) \ (y ` )) & ((x \ (x \ y)) \ (y \ x)) = (((y \ (y \ x)) \ (y \ x)) \ (x \ y)))

    proof

      let X be non empty BCIStr_0;

      thus X is positive-implicative BCI-algebra implies for x,y,z be Element of X holds (((x \ y) \ (x \ z)) \ (z \ y)) = ( 0. X) & (x \ ( 0. X)) = x & (x \ y) = (((x \ y) \ y) \ (y ` )) & ((x \ (x \ y)) \ (y \ x)) = (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) by Lm24, Th1, Th2, Th84;

      assume

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

      now

        let x be Element of X;

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

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

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

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

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

      end;

      then

       A2: X is being_I;

      now

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

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

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

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

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

        hence x = y by A1;

      end;

      then

       A3: X is being_BCI-4;

      now

        let x,y,z be Element of X;

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

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

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

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

      end;

      then X is weakly-positive-implicative BCI-algebra by A1, A2, A3, Th1, Th84;

      hence thesis by Lm25;

    end;