bcialg_2.miz



    begin

    reserve X for BCI-algebra;

    reserve I for Ideal of X;

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

    reserve f,f9,g for sequence of the carrier of X;

    reserve j,i,k,n,m for Nat;

    definition

      let X, x, y;

      let n be Nat;

      :: BCIALG_2:def1

      func (x,y) to_power n -> Element of X means

      : Def1: ex f st it = (f . n) & (f . 0 ) = x & for j be Nat st j < n holds (f . (j + 1)) = ((f . j) \ y);

      existence

      proof

        defpred P[ set] means for x,y be Element of X, n be Nat st n = $1 holds ex u be Element of X st ex f be sequence of the carrier of X st u = (f . n) & (f . 0 ) = x & for j be Nat st j < n holds (f . (j + 1)) = ((f . j) \ y);

        now

          let n be Nat;

          assume

           A1: for x, y, k st k = n holds ex u st ex f st u = (f . k) & (f . 0 ) = x & for j st j < k holds (f . (j + 1)) = ((f . j) \ y);

          let x, y, k;

          consider u, f such that u = (f . n) and

           A2: (f . 0 ) = x and

           A3: for j st j < n holds (f . (j + 1)) = ((f . j) \ y) by A1;

          defpred P[ set, set] means for j st $1 = j holds (j < (n + 1) implies $2 = (f . $1)) & ((n + 1) <= j implies $2 = ((f . n) \ y));

          assume k = (n + 1);

          

           A4: for k be Element of NAT holds ex v be Element of X st P[k, v]

          proof

            let k be Element of NAT ;

            reconsider i = k as Nat;

             A5:

            now

              assume

               A6: (n + 1) <= i;

              take v = ((f . n) \ y);

              let j;

              assume k = j;

              hence j < (n + 1) implies v = (f . k) by A6;

              assume (n + 1) <= j;

              thus v = ((f . n) \ y);

            end;

            now

              assume

               A7: i < (n + 1);

              take v = (f . k);

              let j such that

               A8: k = j;

              thus j < (n + 1) implies v = (f . k);

              thus (n + 1) <= j implies v = ((f . n) \ y) by A7, A8;

            end;

            hence thesis by A5;

          end;

          consider f9 be sequence of the carrier of X such that

           A9: for k be Element of NAT holds P[k, (f9 . k)] from FUNCT_2:sch 3( A4);

          

           A10: for k be Nat holds P[k, (f9 . k)]

          proof

            let k be Nat;

            k in NAT by ORDINAL1:def 12;

            hence thesis by A9;

          end;

          take z = (f9 . (n + 1));

          take f99 = f9;

          thus z = (f99 . (n + 1));

           0 < (n + 1) by NAT_1: 5;

          hence (f99 . 0 ) = x by A2, A10;

          let j;

           A11:

          now

            assume

             A12: j < n;

            then (f . (j + 1)) = ((f . j) \ y) & j < (n + 1) by A3, NAT_1: 13;

            then

             A13: (f . (j + 1)) = ((f9 . j) \ y) by A10;

            (j + 1) < (n + 1) by A12, XREAL_1: 6;

            hence (f99 . (j + 1)) = ((f99 . j) \ y) by A10, A13;

          end;

          

           A14: n < (n + 1) by NAT_1: 13;

           A15:

          now

            assume

             A16: j = n;

            then (f99 . (j + 1)) = ((f . j) \ y) by A10;

            hence (f99 . (j + 1)) = ((f99 . j) \ y) by A14, A10, A16;

          end;

          assume j < (n + 1);

          then j <= n by NAT_1: 13;

          hence (f99 . (j + 1)) = ((f99 . j) \ y) by A11, A15, XXREAL_0: 1;

        end;

        then

         A17: for n be Nat st P[n] holds P[(n + 1)];

        now

          let x,y be Element of X, n be Nat;

          assume

           A18: n = 0 ;

          reconsider f = ( NAT --> x) as sequence of the carrier of X;

          take u = (f . n);

          take f9 = f;

          thus u = (f9 . n) & (f9 . 0 ) = x by FUNCOP_1: 7;

          thus for j be Nat st j < n holds (f9 . (j + 1)) = ((f9 . j) \ y) by A18, NAT_1: 3;

        end;

        then

         A19: P[ 0 ];

        for n holds P[n] from NAT_1:sch 2( A19, A17);

        hence thesis;

      end;

      uniqueness

      proof

        let v1,v2 be Element of X;

        given f such that

         A20: v1 = (f . n) and

         A21: (f . 0 ) = x and

         A22: for j st j < n holds (f . (j + 1)) = ((f . j) \ y);

        given f9 such that

         A23: v2 = (f9 . n) and

         A24: (f9 . 0 ) = x and

         A25: for j st j < n holds (f9 . (j + 1)) = ((f9 . j) \ y);

        defpred P[ Nat] means $1 <= n implies (f . $1) = (f9 . $1);

        now

          let k;

          assume

           A26: k <= n implies (f . k) = (f9 . k);

          assume (k + 1) <= n;

          then

           A27: k < n by NAT_1: 13;

          then (f . (k + 1)) = ((f . k) \ y) by A22;

          hence (f . (k + 1)) = (f9 . (k + 1)) by A25, A26, A27;

        end;

        then

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

        

         A29: P[ 0 ] by A21, A24;

        for k holds P[k] from NAT_1:sch 2( A29, A28);

        hence thesis by A20, A23;

      end;

    end

    theorem :: BCIALG_2:1

    

     Th1: ((x,y) to_power 0 ) = x

    proof

      ex f st ((x,y) to_power 0 ) = (f . 0 ) & (f . 0 ) = x & for j st j < 0 holds (f . (j + 1)) = ((f . j) \ y) by Def1;

      hence thesis;

    end;

    theorem :: BCIALG_2:2

    

     Th2: ((x,y) to_power 1) = (x \ y)

    proof

      consider f such that

       A1: ((x,y) to_power 1) = (f . 1) and

       A2: (f . 0 ) = x & for j st j < 1 holds (f . (j + 1)) = ((f . j) \ y) by Def1;

      (f . ( 0 + 1)) = (x \ y) by A2, NAT_1: 3;

      hence thesis by A1;

    end;

    theorem :: BCIALG_2:3

    ((x,y) to_power 2) = ((x \ y) \ y)

    proof

      consider f such that

       A1: ((x,y) to_power 2) = (f . 2) & (f . 0 ) = x and

       A2: for j st j < 2 holds (f . (j + 1)) = ((f . j) \ y) by Def1;

      1 < (1 + 1) by NAT_1: 13;

      then (f . (1 + 1)) = ((f . ( 0 + 1)) \ y) by A2;

      hence thesis by A1, A2, NAT_1: 3;

    end;

    theorem :: BCIALG_2:4

    

     Th4: ((x,y) to_power (n + 1)) = (((x,y) to_power n) \ y)

    proof

      

       A1: n < (n + 1) by NAT_1: 3, XREAL_1: 29;

      consider g such that

       A2: ((x,y) to_power n) = (g . n) and

       A3: (g . 0 ) = x and

       A4: for j st j < n holds (g . (j + 1)) = ((g . j) \ y) by Def1;

      consider f such that

       A5: ((x,y) to_power (n + 1)) = (f . (n + 1)) and

       A6: (f . 0 ) = x and

       A7: for j st j < (n + 1) holds (f . (j + 1)) = ((f . j) \ y) by Def1;

      defpred P[ set] means for m holds m = $1 & m <= n implies (f . m) = (g . m);

      now

        let k;

        assume

         A8: for m st m = k & m <= n holds (f . m) = (g . m);

        let m;

        assume that

         A9: m = (k + 1) and

         A10: m <= n;

        (k + 1) <= (n + 1) by A9, A10, NAT_1: 13;

        then k < (n + 1) by NAT_1: 13;

        then

         A11: (f . (k + 1)) = ((f . k) \ y) by A7;

        

         A12: k < n by A9, A10, NAT_1: 13;

        then (g . (k + 1)) = ((g . k) \ y) by A4;

        hence (f . m) = (g . m) by A8, A9, A12, A11;

      end;

      then

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

      

       A14: P[ 0 ] by A6, A3;

      for n holds P[n] from NAT_1:sch 2( A14, A13);

      then (f . n) = (g . n);

      hence thesis by A5, A7, A2, A1;

    end;

    theorem :: BCIALG_2:5

    

     Th5: ((x,( 0. X)) to_power (n + 1)) = x

    proof

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

      now

        let k;

        assume

         A1: for m st m = k & m <= n holds ((x,( 0. X)) to_power (m + 1)) = x;

        let m;

        assume that

         A2: m = (k + 1) and

         A3: m <= n;

        ((x,( 0. X)) to_power (m + 1)) = (((x,( 0. X)) to_power (k + 1)) \ ( 0. X)) by A2, Th4;

        then

         A4: ((x,( 0. X)) to_power (m + 1)) = ((x,( 0. X)) to_power (k + 1)) by BCIALG_1: 2;

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

        hence ((x,( 0. X)) to_power (m + 1)) = x by A1, A4;

      end;

      then

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

      ((x,( 0. X)) to_power ( 0 + 1)) = (x \ ( 0. X)) by Th2;

      then

       A6: P[ 0 ] by BCIALG_1: 2;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:6

    

     Th6: ((( 0. X),( 0. X)) to_power n) = ( 0. X)

    proof

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

      

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

      

       A2: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:7

    

     Th7: (((x,y) to_power n) \ z) = (((x \ z),y) to_power n)

    proof

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

      now

        let k;

        assume

         A1: for m st m = k & m <= n holds (((x,y) to_power m) \ z) = (((x \ z),y) to_power m);

        let m;

        assume that

         A2: m = (k + 1) and

         A3: m <= n;

        (((x,y) to_power m) \ z) = ((((x,y) to_power k) \ y) \ z) by A2, Th4;

        then

         A4: (((x,y) to_power m) \ z) = ((((x,y) to_power k) \ z) \ y) by BCIALG_1: 7;

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

        then (((x,y) to_power m) \ z) = ((((x \ z),y) to_power k) \ y) by A1, A4;

        hence (((x,y) to_power m) \ z) = (((x \ z),y) to_power (k + 1)) by Th4;

      end;

      then

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

      (((x,y) to_power 0 ) \ z) = (x \ z) by Th1;

      then

       A6: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:8

    ((x,(x \ (x \ y))) to_power n) = ((x,y) to_power n)

    proof

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

      now

        let k;

        assume

         A1: for m holds m = k & m <= n implies ((x,(x \ (x \ y))) to_power m) = ((x,y) to_power m);

        let m;

        

         A2: ((x,(x \ (x \ y))) to_power (k + 1)) = (((x,(x \ (x \ y))) to_power k) \ (x \ (x \ y))) by Th4;

        assume m = (k + 1) & m <= n;

        then k <= n by NAT_1: 13;

        

        hence ((x,(x \ (x \ y))) to_power (k + 1)) = (((x,y) to_power k) \ (x \ (x \ y))) by A1, A2

        .= (((x \ (x \ (x \ y))),y) to_power k) by Th7

        .= (((x \ y),y) to_power k) by BCIALG_1: 8

        .= (((x,y) to_power k) \ y) by Th7

        .= ((x,y) to_power (k + 1)) by Th4;

      end;

      then

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

      ((x,(x \ (x \ y))) to_power 0 ) = x by Th1;

      then

       A4: P[ 0 ] by Th1;

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: BCIALG_2:9

    

     Th9: (((( 0. X),x) to_power n) ` ) = ((( 0. X),(x ` )) to_power n)

    proof

      defpred P[ set] means for m holds m = $1 & m <= n implies (((( 0. X),x) to_power m) ` ) = ((( 0. X),(x ` )) to_power m);

      now

        let k;

        assume

         A1: for m holds m = k & m <= n implies (((( 0. X),x) to_power m) ` ) = ((( 0. X),(x ` )) to_power m);

        let m;

        

         A2: (((( 0. X),x) to_power (k + 1)) ` ) = ((((( 0. X),x) to_power k) \ x) ` ) by Th4

        .= ((((( 0. X),x) to_power k) ` ) \ (x ` )) by BCIALG_1: 9;

        assume m = (k + 1) & m <= n;

        then k <= n by NAT_1: 13;

        

        hence (((( 0. X),x) to_power (k + 1)) ` ) = (((( 0. X),(x ` )) to_power k) \ (x ` )) by A1, A2

        .= ((( 0. X),(x ` )) to_power (k + 1)) by Th4;

      end;

      then

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

      (((( 0. X),x) to_power 0 ) ` ) = (( 0. X) ` ) by Th1;

      then (((( 0. X),x) to_power 0 ) ` ) = ( 0. X) by BCIALG_1: 2;

      then

       A4: P[ 0 ] by Th1;

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: BCIALG_2:10

    

     Th10: ((((x,y) to_power n),y) to_power m) = ((x,y) to_power (n + m))

    proof

      defpred P[ set] means for m1 be Nat holds m1 = $1 & m1 <= n implies ((((x,y) to_power m1),y) to_power m) = ((x,y) to_power (m1 + m));

      now

        let k;

        assume

         A1: for m1 be Nat st m1 = k & m1 <= n holds ((((x,y) to_power m1),y) to_power m) = ((x,y) to_power (m1 + m));

        let m1 be Nat;

        assume that

         A2: m1 = (k + 1) and

         A3: m1 <= n;

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

        then ((((x,y) to_power k),y) to_power m) = ((x,y) to_power (k + m)) by A1;

        then (((((x,y) to_power k),y) to_power m) \ y) = ((x,y) to_power ((k + m) + 1)) by Th4;

        then (((((x,y) to_power k) \ y),y) to_power m) = ((x,y) to_power ((k + m) + 1)) by Th7;

        hence ((((x,y) to_power m1),y) to_power m) = ((x,y) to_power (m1 + m)) by A2, Th4;

      end;

      then

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

      

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:11

    ((((x,y) to_power n),z) to_power m) = ((((x,z) to_power m),y) to_power n)

    proof

      defpred P[ set] means for m1 be Nat holds m1 = $1 & m1 <= n implies ((((x,y) to_power m1),z) to_power m) = ((((x,z) to_power m),y) to_power m1);

      now

        let k;

        assume

         A1: for m1 be Nat st m1 = k & m1 <= n holds ((((x,y) to_power m1),z) to_power m) = ((((x,z) to_power m),y) to_power m1);

        let m1 be Nat;

        assume m1 = (k + 1) & m1 <= n;

        then k <= n by NAT_1: 13;

        

        then (((((x,y) to_power k),z) to_power m) \ y) = (((((x,z) to_power m),y) to_power k) \ y) by A1

        .= ((((x,z) to_power m),y) to_power (k + 1)) by Th4;

        then ((((x,z) to_power m),y) to_power (k + 1)) = (((((x,y) to_power k) \ y),z) to_power m) by Th7;

        hence ((((x,y) to_power (k + 1)),z) to_power m) = ((((x,z) to_power m),y) to_power (k + 1)) by Th4;

      end;

      then

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

      ((((x,y) to_power 0 ),z) to_power m) = ((x,z) to_power m) by Th1;

      then

       A3: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:12

    

     Th12: ((((( 0. X),x) to_power n) ` ) ` ) = ((( 0. X),x) to_power n)

    proof

      defpred P[ set] means for m be Nat holds m = $1 & m <= n implies ((((( 0. X),x) to_power m) ` ) ` ) = ((( 0. X),x) to_power m);

      now

        let k;

        assume

         A1: for m be Nat st m = k & m <= n holds ((((( 0. X),x) to_power m) ` ) ` ) = ((( 0. X),x) to_power m);

        let m be Nat;

        assume m = (k + 1) & m <= n;

        then

         A2: k <= n by NAT_1: 13;

        ((((( 0. X),x) to_power (k + 1)) ` ) ` ) = (((((( 0. X),x) to_power k) \ x) ` ) ` ) by Th4

        .= (((((( 0. X),x) to_power k) ` ) \ (x ` )) ` ) by BCIALG_1: 9

        .= (((((( 0. X),x) to_power k) ` ) ` ) \ ((x ` ) ` )) by BCIALG_1: 9

        .= (((( 0. X),x) to_power k) \ ((x ` ) ` )) by A1, A2

        .= (((((x ` ) ` ) ` ),x) to_power k) by Th7

        .= (((x ` ),x) to_power k) by BCIALG_1: 8

        .= (((( 0. X),x) to_power k) \ x) by Th7;

        hence ((((( 0. X),x) to_power (k + 1)) ` ) ` ) = ((( 0. X),x) to_power (k + 1)) by Th4;

      end;

      then

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

      ((((( 0. X),x) to_power 0 ) ` ) ` ) = ((( 0. X) ` ) ` ) by Th1

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

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

      then

       A4: P[ 0 ] by Th1;

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: BCIALG_2:13

    

     Th13: ((( 0. X),x) to_power (n + m)) = (((( 0. X),x) to_power n) \ (((( 0. X),x) to_power m) ` ))

    proof

      defpred P[ set] means for j be Nat holds j = $1 & j <= n implies ((( 0. X),x) to_power (j + m)) = (((( 0. X),x) to_power j) \ (((( 0. X),x) to_power m) ` ));

      now

        let k;

        assume

         A1: for j be Nat st j = k & j <= n holds ((( 0. X),x) to_power (j + m)) = (((( 0. X),x) to_power j) \ (((( 0. X),x) to_power m) ` ));

        let j be Nat;

        assume j = (k + 1) & j <= n;

        then

         A2: k <= n by NAT_1: 13;

        ((( 0. X),x) to_power ((k + m) + 1)) = (((( 0. X),x) to_power (k + m)) \ x) by Th4

        .= ((((( 0. X),x) to_power k) \ (((( 0. X),x) to_power m) ` )) \ x) by A1, A2

        .= ((((( 0. X),x) to_power k) \ x) \ (((( 0. X),x) to_power m) ` )) by BCIALG_1: 7;

        hence ((( 0. X),x) to_power ((k + 1) + m)) = (((( 0. X),x) to_power (k + 1)) \ (((( 0. X),x) to_power m) ` )) by Th4;

      end;

      then

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

      ((( 0. X),x) to_power ( 0 + m)) = ((((( 0. X),x) to_power m) ` ) ` ) by Th12;

      then

       A4: P[ 0 ] by Th1;

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: BCIALG_2:14

    (((( 0. X),x) to_power (m + n)) ` ) = ((((( 0. X),x) to_power m) ` ) \ ((( 0. X),x) to_power n))

    proof

      (((( 0. X),x) to_power (m + n)) ` ) = ((((( 0. X),x) to_power m) \ (((( 0. X),x) to_power n) ` )) ` ) by Th13

      .= ((((( 0. X),x) to_power m) ` ) \ ((((( 0. X),x) to_power n) ` ) ` )) by BCIALG_1: 9;

      hence thesis by Th12;

    end;

    theorem :: BCIALG_2:15

    (((( 0. X),((( 0. X),x) to_power m)) to_power n) ` ) = ((( 0. X),x) to_power (m * n))

    proof

      defpred P[ set] means for j be Nat holds j = $1 & j <= n implies (((( 0. X),((( 0. X),x) to_power m)) to_power j) ` ) = ((( 0. X),x) to_power (m * j));

      now

        let k;

        assume

         A1: for j be Nat st j = k & j <= n holds (((( 0. X),((( 0. X),x) to_power m)) to_power j) ` ) = ((( 0. X),x) to_power (m * j));

        let j be Nat;

        assume j = (k + 1) & j <= n;

        then

         A2: k <= n by NAT_1: 13;

        (((( 0. X),((( 0. X),x) to_power m)) to_power (k + 1)) ` ) = ((((( 0. X),((( 0. X),x) to_power m)) to_power k) \ ((( 0. X),x) to_power m)) ` ) by Th4

        .= ((((( 0. X),((( 0. X),x) to_power m)) to_power k) ` ) \ (((( 0. X),x) to_power m) ` )) by BCIALG_1: 9

        .= (((( 0. X),x) to_power (m * k)) \ (((( 0. X),x) to_power m) ` )) by A1, A2

        .= ((( 0. X),x) to_power ((m * k) + m)) by Th13;

        hence (((( 0. X),((( 0. X),x) to_power m)) to_power (k + 1)) ` ) = ((( 0. X),x) to_power (m * (k + 1)));

      end;

      then

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

      (((( 0. X),((( 0. X),x) to_power m)) to_power 0 ) ` ) = (( 0. X) ` ) by Th1

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

      then

       A4: P[ 0 ] by Th1;

      for n holds P[n] from NAT_1:sch 2( A4, A3);

      hence thesis;

    end;

    theorem :: BCIALG_2:16

    ((( 0. X),x) to_power m) = ( 0. X) implies ((( 0. X),x) to_power (m * n)) = ( 0. X)

    proof

      defpred P[ set] means for j be Nat holds j = $1 & j <= n implies ((( 0. X),x) to_power (m * j)) = ( 0. X);

      assume

       A1: ((( 0. X),x) to_power m) = ( 0. X);

      now

        let k;

        assume

         A2: for j st j = k & j <= n holds ((( 0. X),x) to_power (m * j)) = ( 0. X);

        let j;

        assume j = (k + 1) & j <= n;

        then

         A3: k <= n by NAT_1: 13;

        ((( 0. X),x) to_power (m * (k + 1))) = ((( 0. X),x) to_power ((m * k) + m))

        .= ((((( 0. X),x) to_power (m * k)),x) to_power m) by Th10

        .= ((( 0. X),x) to_power m) by A2, A3;

        hence ((( 0. X),x) to_power (m * (k + 1))) = ( 0. X) by A1;

      end;

      then

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

      

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:17

    (x \ y) = x implies ((x,y) to_power n) = x

    proof

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

      assume

       A1: (x \ y) = x;

      now

        let k;

        assume

         A2: for m holds m = k & m <= n implies ((x,y) to_power m) = x;

        let m;

        

         A3: ((x,y) to_power (k + 1)) = (((x,y) to_power k) \ y) by Th4;

        assume m = (k + 1) & m <= n;

        then k <= n by NAT_1: 13;

        hence ((x,y) to_power (k + 1)) = x by A1, A2, A3;

      end;

      then

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

      

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:18

    ((( 0. X),(x \ y)) to_power n) = (((( 0. X),x) to_power n) \ ((( 0. X),y) to_power n))

    proof

      defpred P[ set] means for m holds m = $1 & m <= n implies ((( 0. X),(x \ y)) to_power m) = (((( 0. X),x) to_power m) \ ((( 0. X),y) to_power m));

      

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

      proof

        let k;

        assume

         A2: for m holds m = k & m <= n implies ((( 0. X),(x \ y)) to_power m) = (((( 0. X),x) to_power m) \ ((( 0. X),y) to_power m));

        let m;

        assume that

         A3: m = (k + 1) and

         A4: m <= n;

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

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

        

        then ((( 0. X),(x \ y)) to_power (k + 1)) = ((((( 0. X),x) to_power k) \ ((( 0. X),y) to_power k)) \ (x \ y)) by Th4

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

        .= (((((x \ y) ` ),x) to_power k) \ ((( 0. X),y) to_power k)) by Th7

        .= (((((x ` ) \ (y ` )),x) to_power k) \ ((( 0. X),y) to_power k)) by BCIALG_1: 9

        .= (((((x ` ),x) to_power k) \ (y ` )) \ ((( 0. X),y) to_power k)) by Th7

        .= (((((x ` ),x) to_power k) \ ((( 0. X),y) to_power k)) \ (y ` )) by BCIALG_1: 7

        .= (((((( 0. X),x) to_power k) \ x) \ ((( 0. X),y) to_power k)) \ (y ` )) by Th7;

        

        then ((( 0. X),(x \ y)) to_power (k + 1)) = ((((( 0. X),x) to_power (k + 1)) \ ((( 0. X),y) to_power k)) \ (y ` )) by Th4

        .= ((((( 0. X),x) to_power (k + 1)) \ (y ` )) \ ((( 0. X),y) to_power k)) by BCIALG_1: 7

        .= (((((y ` ) ` ),x) to_power (k + 1)) \ ((( 0. X),y) to_power k)) by Th7

        .= (((((y ` ) ` ) \ ((( 0. X),y) to_power k)),x) to_power (k + 1)) by Th7

        .= ((((((( 0. X),y) to_power k) ` ) \ (y ` )),x) to_power (k + 1)) by BCIALG_1: 7

        .= ((((((( 0. X),y) to_power k) \ y) ` ),x) to_power (k + 1)) by BCIALG_1: 9

        .= (((((( 0. X),y) to_power (k + 1)) ` ),x) to_power (k + 1)) by Th4;

        hence thesis by A3, Th7;

      end;

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

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

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

      then

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:19

    x <= y implies ((x,z) to_power n) <= ((y,z) to_power n)

    proof

      defpred P[ set] means for m be Nat holds m = $1 & m <= n implies ((x,z) to_power m) <= ((y,z) to_power m);

      

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

      proof

        let k;

        assume

         A2: for m be Nat holds m = k & m <= n implies ((x,z) to_power m) <= ((y,z) to_power m);

        let m be Nat;

        assume that

         A3: m = (k + 1) and

         A4: m <= n;

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

        then ((x,z) to_power k) <= ((y,z) to_power k) by A2;

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

        then ((x,z) to_power (k + 1)) <= (((y,z) to_power k) \ z) by Th4;

        hence thesis by A3, Th4;

      end;

      assume x <= y;

      then ((x,z) to_power 0 ) <= y by Th1;

      then

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:20

    x <= y implies ((z,y) to_power n) <= ((z,x) to_power n)

    proof

      defpred P[ set] means for m be Nat holds m = $1 & m <= n implies ((z,y) to_power m) <= ((z,x) to_power m);

      assume

       A1: x <= y;

      

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

      proof

        let k;

        assume

         A3: for m holds m = k & m <= n implies ((z,y) to_power m) <= ((z,x) to_power m);

        (((z,x) to_power k) \ y) <= (((z,x) to_power k) \ x) by A1, BCIALG_1: 5;

        then (((z,x) to_power k) \ y) <= ((z,x) to_power (k + 1)) by Th4;

        then

         A4: ((((z,x) to_power k) \ y) \ ((z,x) to_power (k + 1))) = ( 0. X);

        let m;

        assume that

         A5: m = (k + 1) and

         A6: m <= n;

        k <= n by A5, A6, NAT_1: 13;

        then ((z,y) to_power k) <= ((z,x) to_power k) by A3;

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

        then ((z,y) to_power (k + 1)) <= (((z,x) to_power k) \ y) by Th4;

        then (((z,y) to_power (k + 1)) \ (((z,x) to_power k) \ y)) = ( 0. X);

        then (((z,y) to_power (k + 1)) \ ((z,x) to_power (k + 1))) = ( 0. X) by A4, BCIALG_1: 3;

        hence thesis by A5;

      end;

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

      then z <= z;

      then ((z,y) to_power 0 ) <= z by Th1;

      then

       A7: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:21

    (((x,z) to_power n) \ ((y,z) to_power n)) <= (x \ y)

    proof

      defpred P[ set] means for m be Nat holds m = $1 & m <= n implies (((x,z) to_power m) \ ((y,z) to_power m)) <= (x \ y);

      

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

      proof

        let k;

        assume

         A2: for m be Nat holds m = k & m <= n implies (((x,z) to_power m) \ ((y,z) to_power m)) <= (x \ y);

        let m be Nat;

        assume that

         A3: m = (k + 1) and

         A4: m <= n;

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

        then (((x,z) to_power k) \ ((y,z) to_power k)) <= (x \ y) by A2;

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

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

        then (((((x,z) to_power k) \ (x \ y)) \ z) \ (((y,z) to_power k) \ z)) = ( 0. X) by BCIALG_1: 4;

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

        then ((((x,z) to_power (k + 1)) \ (x \ y)) \ (((y,z) to_power k) \ z)) = ( 0. X) by Th4;

        then ((((x,z) to_power (k + 1)) \ (x \ y)) \ ((y,z) to_power (k + 1))) = ( 0. X) by Th4;

        then ((((x,z) to_power (k + 1)) \ ((y,z) to_power (k + 1))) \ (x \ y)) = ( 0. X) by BCIALG_1: 7;

        hence thesis by A3;

      end;

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

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

      then (((x,z) to_power 0 ) \ y) <= (x \ y) by Th1;

      then

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:22

    ((((x,(x \ y)) to_power n),(y \ x)) to_power n) <= x

    proof

      defpred P[ set] means for m be Nat holds m = $1 & m <= n implies ((((x,(x \ y)) to_power m),(y \ x)) to_power m) <= x;

      

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

      proof

        let k;

        assume

         A2: for m be Nat holds m = k & m <= n implies ((((x,(x \ y)) to_power m),(y \ x)) to_power m) <= x;

        let m be Nat;

        assume that

         A3: m = (k + 1) and

         A4: m <= n;

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

        then ((((x,(x \ y)) to_power k),(y \ x)) to_power k) <= x by A2;

        then (((((x,(x \ y)) to_power k),(y \ x)) to_power k) \ x) = ( 0. X);

        then ((((((x,(x \ y)) to_power k) \ x),(y \ x)) to_power k) \ (y \ x)) = ((y \ x) ` ) by Th7;

        then ((((((x,(x \ y)) to_power k) \ x),(y \ x)) to_power (k + 1)) \ (x \ y)) = (((y \ x) ` ) \ (x \ y)) by Th4;

        then ((((((x,(x \ y)) to_power k) \ x) \ (x \ y)),(y \ x)) to_power (k + 1)) = (((y \ x) ` ) \ (x \ y)) by Th7;

        then ((((((x,(x \ y)) to_power k) \ (x \ y)) \ x),(y \ x)) to_power (k + 1)) = (((y \ x) ` ) \ (x \ y)) by BCIALG_1: 7;

        then (((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1)) = (((y \ x) ` ) \ (x \ y)) by Th4;

        then (((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1)) = (((y \ y) \ (y \ x)) \ (x \ y)) by BCIALG_1:def 5;

        then (((((x,(x \ y)) to_power (k + 1)) \ x),(y \ x)) to_power (k + 1)) = ( 0. X) by BCIALG_1: 1;

        then (((((x,(x \ y)) to_power (k + 1)),(y \ x)) to_power (k + 1)) \ x) = ( 0. X) by Th7;

        hence thesis by A3;

      end;

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

      then x <= x;

      then ((x,(y \ x)) to_power 0 ) <= x by Th1;

      then

       A5: P[ 0 ] by Th1;

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

      hence thesis;

    end;

    notation

      let X, a;

      synonym a is minimal for a is atom;

    end

    definition

      let X, a;

      :: BCIALG_2:def2

      attr a is positive means

      : Def2: ( 0. X) <= a;

      :: BCIALG_2:def3

      attr a is least means for x holds a <= x;

      :: BCIALG_2:def4

      attr a is maximal means for x holds a <= x implies x = a;

      :: BCIALG_2:def5

      attr a is greatest means for x holds x <= a;

    end

    

     Lm1: a is minimal iff for x holds x <= a implies x = a by BCIALG_1:def 11;

    

     Lm2: ( 0. X) is positive

    proof

      (( 0. X) ` ) = ( 0. X) by BCIALG_1: 2;

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

      hence thesis;

    end;

    registration

      let X;

      cluster positive for Element of X;

      existence

      proof

        take ( 0. X);

        thus thesis by Lm2;

      end;

    end

    

     Lm3: ( 0. X) is minimal by BCIALG_1: 2;

    registration

      let X;

      cluster ( 0. X) -> positive minimal;

      coherence by Lm2, Lm3;

    end

    theorem :: BCIALG_2:23

    a is minimal iff for x holds (a \ x) = ((x ` ) \ (a ` ))

    proof

      thus a is minimal implies for x holds (a \ x) = ((x ` ) \ (a ` ))

      proof

        assume

         A1: a is minimal;

        let x;

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

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

        

        then

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

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

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

        .= (((x \ a) ` ) \ ((x \ a) ` )) by BCIALG_1: 9

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

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

        hence thesis by A2, BCIALG_1:def 7;

      end;

      thus (for x holds (a \ x) = ((x ` ) \ (a ` ))) implies a is minimal

      proof

        assume

         A3: for x holds (a \ x) = ((x ` ) \ (a ` ));

        now

          let x;

          assume x <= a;

          then

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

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

          then (a \ x) = (( 0. X) ` ) by A4, BCIALG_1: 9;

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

          hence a = x by A4, BCIALG_1:def 7;

        end;

        hence thesis by Lm1;

      end;

    end;

    theorem :: BCIALG_2:24

    (x ` ) is minimal iff for y holds y <= x implies (x ` ) = (y ` )

    proof

      thus (x ` ) is minimal implies for y holds y <= x implies (x ` ) = (y ` )

      proof

        assume

         A1: (x ` ) is minimal;

        let y;

        assume y <= x;

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

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

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

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

        hence thesis by A1;

      end;

      thus (for y holds y <= x implies (x ` ) = (y ` )) implies (x ` ) is minimal

      proof

        assume

         A2: for y holds y <= x implies (x ` ) = (y ` );

        now

          let xx be Element of X;

          assume xx <= (x ` );

          then

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

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

          then ((xx ` ) \ ((x ` ) ` )) = ( 0. X) by BCIALG_1: 9;

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

          then (((xx ` ) ` ) \ (((x ` ) ` ) ` )) = ( 0. X) by BCIALG_1: 9;

          then (((xx ` ) ` ) \ (x ` )) = ( 0. X) by BCIALG_1: 8;

          then (((xx ` ) \ x) ` ) = ( 0. X) by BCIALG_1: 9;

          then (((x ` ) \ xx) ` ) = ( 0. X) by BCIALG_1: 7;

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

          then ((xx \ (x ` )) ` ) = ( 0. X) by BCIALG_1:def 3;

          then ((xx ` ) \ ((x ` ) ` )) = ( 0. X) by BCIALG_1: 9;

          then (((xx ` ) \ x) \ (((x ` ) ` ) \ x)) = ( 0. X) by BCIALG_1: 4;

          then (((xx ` ) \ x) \ ( 0. X)) = ( 0. X) by BCIALG_1: 1;

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

          then (xx ` ) <= x;

          then ((xx ` ) ` ) = (x ` ) by A2;

          then ( 0. X) = ((x ` ) \ xx) by BCIALG_1: 1;

          hence xx = (x ` ) by A3, BCIALG_1:def 7;

        end;

        hence thesis by Lm1;

      end;

    end;

    theorem :: BCIALG_2:25

    (x ` ) is minimal iff for y, z holds ((((x \ z) \ (y \ z)) ` ) ` ) = ((y ` ) \ (x ` ))

    proof

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

      proof

        assume

         A1: (x ` ) is minimal;

        let y, z;

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

        then

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

        ((((x \ z) \ (y \ z)) ` ) ` ) = ((((x \ z) ` ) \ ((y \ z) ` )) ` ) by BCIALG_1: 9

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

        

        then ((((x \ z) \ (y \ z)) ` ) ` ) = (((((y ` ) \ (x \ y)) \ (z ` )) \ ((y \ z) ` )) ` ) by A1, A2

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

        .= (((((y \ z) ` ) \ (x \ y)) \ ((y \ z) ` )) ` ) by BCIALG_1: 9

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

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

        .= (((x ` ) \ (y ` )) ` ) by BCIALG_1: 9

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

        .= ((((y ` ) ` ) ` ) \ (x ` )) by BCIALG_1: 9

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

        hence thesis;

      end;

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

      proof

        assume

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

        now

          let x1 be Element of X;

          assume x1 <= (x ` );

          then

           A4: (x1 \ (x ` )) = ( 0. X);

          then (((x1 ` ) \ (x ` )) \ ((x1 ` ) \ x1)) = ( 0. X) by BCIALG_1: 4;

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

          then ((((x1 ` ) \ x1) ` ) \ (((x \ ( 0. X)) \ (x1 \ ( 0. X))) ` )) = ( 0. X) by BCIALG_1: 7;

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

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

          then ((((x1 ` ) ` ) \ (x1 ` )) \ ((x \ x1) ` )) = ( 0. X) by BCIALG_1: 9;

          then ((((x1 ` ) ` ) \ (x1 ` )) \ ((x ` ) \ (x1 ` ))) = ( 0. X) by BCIALG_1: 9;

          then ((((x1 ` ) ` ) \ (x ` )) ` ) = ( 0. X) by BCIALG_1:def 3;

          then ((((x1 ` ) ` ) ` ) \ ((x ` ) ` )) = ( 0. X) by BCIALG_1: 9;

          then ((x1 ` ) \ ((x ` ) ` )) = ( 0. X) by BCIALG_1: 8;

          then ((((x ` ) ` ) ` ) \ x1) = ( 0. X) by BCIALG_1: 7;

          then ((x ` ) \ x1) = ( 0. X) by BCIALG_1: 8;

          hence x1 = (x ` ) by A4, BCIALG_1:def 7;

        end;

        hence thesis by Lm1;

      end;

    end;

    theorem :: BCIALG_2:26

    ( 0. X) is maximal implies for a holds a is minimal

    proof

      assume

       A1: ( 0. X) is maximal;

      let a;

      now

        let x;

        assume x <= a;

        then

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

        then ((a \ x) ` ) = ( 0. X) by BCIALG_1: 6;

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

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

        hence x = a by A2, BCIALG_1:def 7;

      end;

      hence thesis by Lm1;

    end;

    theorem :: BCIALG_2:27

    (ex x st x is greatest) implies for a holds a is positive

    proof

      given x such that

       A1: x is greatest;

      let a;

      a <= x by A1;

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

      then

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

      ( 0. X) <= x by A1;

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

      then ((a ` ) \ ( 0. X)) = ( 0. X) by A2, BCIALG_1: 9;

      then (a ` ) = ( 0. X) by BCIALG_1: 2;

      then ( 0. X) <= a;

      hence thesis;

    end;

    theorem :: BCIALG_2:28

    

     Th28: (x \ ((x ` ) ` )) is positive Element of X

    proof

      ((x \ ((x ` ) ` )) ` ) = ((x ` ) \ (((x ` ) ` ) ` )) by BCIALG_1: 9

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

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

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

      hence thesis by Def2;

    end;

    theorem :: BCIALG_2:29

    a is minimal iff ((a ` ) ` ) = a

    proof

      thus a is minimal implies ((a ` ) ` ) = a

      proof

        (((a ` ) ` ) \ a) = ( 0. X) by BCIALG_1: 1;

        then

         A1: ((a ` ) ` ) <= a;

        assume a is minimal;

        hence thesis by A1;

      end;

      assume

       A2: ((a ` ) ` ) = a;

      now

        let x;

        assume x <= a;

        then

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

        (a \ x) = ((x ` ) \ (a ` )) by A2, BCIALG_1: 7;

        then (a \ x) = (( 0. X) ` ) by A3, BCIALG_1: 9;

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

        hence x = a by A3, BCIALG_1:def 7;

      end;

      hence thesis by Lm1;

    end;

    theorem :: BCIALG_2:30

    

     Th30: a is minimal iff ex x st a = (x ` )

    proof

      thus a is minimal implies ex x st a = (x ` )

      proof

        assume

         A1: a is minimal;

        take x = (a ` );

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

        then (x ` ) <= a;

        hence thesis by A1;

      end;

      given x such that

       A2: a = (x ` );

      now

        let y;

        assume y <= a;

        then

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

        then (a \ y) = (((y \ (x ` )) \ y) \ x) by A2, BCIALG_1: 7;

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

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

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

        hence a = y by A3, BCIALG_1:def 7;

      end;

      hence thesis by Lm1;

    end;

    definition

      let X, x;

      :: BCIALG_2:def6

      attr x is nilpotent means ex k be non zero Nat st ((( 0. X),x) to_power k) = ( 0. X);

    end

    definition

      let X;

      :: BCIALG_2:def7

      attr X is nilpotent means for x be Element of X holds x is nilpotent;

    end

    definition

      let X, x;

      assume

       A1: x is nilpotent;

      :: BCIALG_2:def8

      func ord x -> non zero Nat means

      : Def8: ((( 0. X),x) to_power it ) = ( 0. X) & for m be Nat st ((( 0. X),x) to_power m) = ( 0. X) & m <> 0 holds it <= m;

      existence

      proof

        defpred P[ Nat] means ex w be Nat st w = $1 & ((( 0. X),x) to_power w) = ( 0. X) & w <> 0 ;

        ex k be non zero Nat st ((( 0. X),x) to_power k) = ( 0. X) by A1;

        then

         A2: ex n be Nat st P[n];

        consider k be Nat such that

         A3: P[k] and

         A4: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A2);

        reconsider k as non zero Nat by A3;

        take k;

        thus thesis by A3, A4;

      end;

      uniqueness

      proof

        let n1,n2 be non zero Nat;

        assume ((( 0. X),x) to_power n1) = ( 0. X) & (for m be Nat st ((( 0. X),x) to_power m) = ( 0. X) & m <> 0 holds n1 <= m) & ((( 0. X),x) to_power n2) = ( 0. X) & for m be Nat st ((( 0. X),x) to_power m) = ( 0. X) & m <> 0 holds n2 <= m;

        then n1 <= n2 & n2 <= n1;

        hence thesis by XXREAL_0: 1;

      end;

      correctness ;

    end

    registration

      let X;

      cluster ( 0. X) -> nilpotent;

      coherence

      proof

        ((( 0. X),( 0. X)) to_power 1) = ( 0. X) by Th6;

        hence thesis;

      end;

    end

    theorem :: BCIALG_2:31

    x is positive Element of X iff x is nilpotent & ( ord x) = 1

    proof

      thus x is positive Element of X implies x is nilpotent & ( ord x) = 1

      proof

        assume x is positive Element of X;

        then ( 0. X) <= x by Def2;

        then

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

        thus

         A2: x is nilpotent

        proof

          set k = 1;

          take k;

          thus thesis by A1, Th2;

        end;

        thus ( ord x) = 1

        proof

          set k = 1;

          reconsider k as non zero Nat;

          ((( 0. X),x) to_power k) = ( 0. X) & for m be Nat st ((( 0. X),x) to_power m) = ( 0. X) & m <> 0 holds k <= m by A1, Th2, NAT_1: 14;

          hence thesis by A2, Def8;

        end;

      end;

      assume x is nilpotent & ( ord x) = 1;

      then ((( 0. X),x) to_power 1) = ( 0. X) by Def8;

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

      then ( 0. X) <= x;

      hence thesis by Def2;

    end;

    theorem :: BCIALG_2:32

    X is BCK-algebra iff for x holds ( ord x) = 1 & x is nilpotent

    proof

      thus X is BCK-algebra implies for x be Element of X holds ( ord x) = 1 & x is nilpotent

      proof

        set k = 1;

        assume

         A1: X is BCK-algebra;

        let x be Element of X;

        

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

        then ((( 0. X),x) to_power 1) = ( 0. X) by Th2;

        then

         A3: x is nilpotent;

        reconsider k as non zero Nat;

        

         A4: for m be Nat st ((( 0. X),x) to_power m) = ( 0. X) & m <> 0 holds k <= m by NAT_1: 14;

        ((( 0. X),x) to_power k) = ( 0. X) by A2, Th2;

        hence thesis by A3, A4, Def8;

      end;

      assume

       A5: for x holds ( ord x) = 1 & x is nilpotent;

      now

        let x;

        ( ord x) = 1 & x is nilpotent by A5;

        then ((( 0. X),x) to_power 1) = ( 0. X) by Def8;

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

      end;

      hence thesis by BCIALG_1:def 8;

    end;

    theorem :: BCIALG_2:33

    ((( 0. X),(x ` )) to_power n) is minimal

    proof

      ((( 0. X),(x ` )) to_power n) = (((( 0. X),x) to_power n) ` ) by Th9;

      hence thesis by Th30;

    end;

    theorem :: BCIALG_2:34

    x is nilpotent implies ( ord x) = ( ord (x ` ))

    proof

      assume

       A1: x is nilpotent;

      then

      consider k be non zero Nat such that

       A2: ((( 0. X),x) to_power k) = ( 0. X);

      

       A3: (x ` ) is nilpotent

      proof

        take k;

        ((( 0. X),(x ` )) to_power k) = (((( 0. X),x) to_power k) ` ) by Th9

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

        hence thesis;

      end;

      set k = ( ord x);

       A4:

      now

        let m be Nat;

        assume that

         A5: ((( 0. X),(x ` )) to_power m) = ( 0. X) and

         A6: m <> 0 ;

        (((( 0. X),x) to_power m) ` ) = ( 0. X) by A5, Th9;

        then ((((( 0. X),x) to_power m) ` ) ` ) = ( 0. X) by BCIALG_1:def 5;

        then ((( 0. X),x) to_power m) = ( 0. X) by Th12;

        hence k <= m by A1, A6, Def8;

      end;

      ((( 0. X),(x ` )) to_power k) = (((( 0. X),x) to_power k) ` ) by Th9

      .= (( 0. X) ` ) by A1, Def8

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

      hence thesis by A3, A4, Def8;

    end;

    begin

    definition

      let X be BCI-algebra;

      :: BCIALG_2:def9

      mode Congruence of X -> Equivalence_Relation of X means

      : Def9: for x,y,u,v be Element of X st [x, y] in it & [u, v] in it holds [(x \ u), (y \ v)] in it ;

      existence

      proof

        reconsider P = ( id the carrier of X) as Equivalence_Relation of X;

        take P;

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

        assume [x, y] in P & [u, v] in P;

        then x = y & u = v by RELAT_1:def 10;

        hence thesis by RELAT_1:def 10;

      end;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_2:def10

      mode L-congruence of X -> Equivalence_Relation of X means

      : Def10: for x,y be Element of X st [x, y] in it holds for u be Element of X holds [(u \ x), (u \ y)] in it ;

      existence

      proof

        reconsider P = ( id the carrier of X) as Equivalence_Relation of X;

        take P;

        let x,y be Element of X;

        assume

         A1: [x, y] in P;

        let u be Element of X;

        (u \ x) = (u \ y) by A1, RELAT_1:def 10;

        hence thesis by RELAT_1:def 10;

      end;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_2:def11

      mode R-congruence of X -> Equivalence_Relation of X means

      : Def11: for x,y be Element of X st [x, y] in it holds for u be Element of X holds [(x \ u), (y \ u)] in it ;

      existence

      proof

        reconsider P = ( id the carrier of X) as Equivalence_Relation of X;

        take P;

        let x,y be Element of X;

        assume

         A1: [x, y] in P;

        let u be Element of X;

        (x \ u) = (y \ u) by A1, RELAT_1:def 10;

        hence thesis by RELAT_1:def 10;

      end;

    end

    definition

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

      :: BCIALG_2:def12

      mode I-congruence of X,A -> Relation of X means

      : Def12: for x,y be Element of X holds [x, y] in it iff (x \ y) in A & (y \ x) in A;

      existence

      proof

        defpred PP[ object, object] means ex x,y be Element of X st x = $1 & y = $2 & (x \ y) in A & (y \ x) in A;

        consider P be Relation of X such that

         A1: for x2,y2 be object holds [x2, y2] in P iff x2 in the carrier of X & y2 in the carrier of X & PP[x2, y2] from RELSET_1:sch 1;

        take P;

        let x2,y2 be Element of X;

         [x2, y2] in P implies ex x1,y1 be Element of X st x1 = x2 & y1 = y2 & (x1 \ y1) in A & (y1 \ x1) in A by A1;

        hence [x2, y2] in P implies (x2 \ y2) in A & (y2 \ x2) in A;

        thus thesis by A1;

      end;

    end

    registration

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

      cluster -> total symmetric transitive for I-congruence of X, A;

      coherence

      proof

        for RI be I-congruence of X, A holds RI is Equivalence_Relation of X

        proof

          let RI be I-congruence of X, A;

          reconsider RI as Relation of X;

          for x be object st x in the carrier of X holds [x, x] in RI

          proof

            let x be object;

            assume x in the carrier of X;

            then

            reconsider x as Element of X;

            ( 0. X) in A by BCIALG_1:def 18;

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

            hence thesis by Def12;

          end;

          then RI is_reflexive_in the carrier of X by RELAT_2:def 1;

          then

           A1: ( field RI) = the carrier of X by ORDERS_1: 13;

          for x,y,z be object st [x, y] in RI & [y, z] in RI holds [x, z] in RI

          proof

            let x,y,z be object;

            assume that

             A2: [x, y] in RI and

             A3: [y, z] in RI;

            reconsider x, y, z as Element of X by A2, A3, ZFMISC_1: 87;

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

            then

             A4: (((z \ x) \ (y \ x)) \ (z \ y)) in A by BCIALG_1:def 18;

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

            then

             A5: (((x \ z) \ (x \ y)) \ (y \ z)) in A by BCIALG_1:def 18;

            (y \ z) in A by A3, Def12;

            then

             A6: ((x \ z) \ (x \ y)) in A by A5, BCIALG_1:def 18;

            (z \ y) in A by A3, Def12;

            then

             A7: ((z \ x) \ (y \ x)) in A by A4, BCIALG_1:def 18;

            (y \ x) in A by A2, Def12;

            then

             A8: (z \ x) in A by A7, BCIALG_1:def 18;

            (x \ y) in A by A2, Def12;

            then (x \ z) in A by A6, BCIALG_1:def 18;

            hence thesis by A8, Def12;

          end;

          then

           A9: RI is transitive by RELAT_2: 31;

          for x,y be object st x in the carrier of X & y in the carrier of X & [x, y] in RI holds [y, x] in RI

          proof

            let x,y be object;

            assume that

             A10: x in the carrier of X & y in the carrier of X and

             A11: [x, y] in RI;

            reconsider x, y as Element of X by A10;

            (x \ y) in A & (y \ x) in A by A11, Def12;

            hence thesis by Def12;

          end;

          then RI is_symmetric_in the carrier of X by RELAT_2:def 3;

          then RI is symmetric by A1, RELAT_2:def 11;

          hence thesis by A1, A9, EQREL_1: 9;

        end;

        hence thesis;

      end;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_2:def13

      func IConSet (X) -> set means

      : Def13: for A1 be set holds A1 in it iff ex I be Ideal of X st A1 is I-congruence of X, I;

      existence

      proof

        defpred P[ object] means ex I be Ideal of X st $1 is I-congruence of X, I;

        consider Y be set such that

         A1: for x be object holds x in Y iff x in ( bool [:the carrier of X, the carrier of X:]) & P[x] from XBOOLE_0:sch 1;

        take Y;

        let x be set;

        thus x in Y implies ex I be Ideal of X st x is I-congruence of X, I by A1;

        given I be Ideal of X such that

         A2: x is I-congruence of X, I;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ object] means ex I be Ideal of X st $1 is I-congruence of X, I;

        let A1,A2 be set such that

         A3: for x be set holds x in A1 iff ex I be Ideal of X st x is I-congruence of X, I and

         A4: for x be set holds x in A2 iff ex I be Ideal of X st x is I-congruence of X, I;

        

         A5: for x be object holds x in A2 iff P[x] by A4;

        

         A6: for x be object holds x in A1 iff P[x] by A3;

        A1 = A2 from XBOOLE_0:sch 2( A6, A5);

        hence thesis;

      end;

    end

    definition

      let X be BCI-algebra;

      :: BCIALG_2:def14

      func ConSet (X) -> set equals the set of all R where R be Congruence of X;

      coherence ;

      :: BCIALG_2:def15

      func LConSet (X) -> set equals the set of all R where R be L-congruence of X;

      coherence ;

      :: BCIALG_2:def16

      func RConSet (X) -> set equals the set of all R where R be R-congruence of X;

      coherence ;

    end

    reserve R for Equivalence_Relation of X;

    reserve RI for I-congruence of X, I;

    reserve E for Congruence of X;

    reserve RC for R-congruence of X;

    reserve LC for L-congruence of X;

    theorem :: BCIALG_2:35

    for X, E holds ( Class (E,( 0. X))) is closed Ideal of X

    proof

      let X, E;

       A1:

      now

        let x,y be Element of X;

        assume that

         A2: (x \ y) in ( Class (E,( 0. X))) and

         A3: y in ( Class (E,( 0. X)));

        

         A4: [x, x] in E by EQREL_1: 5;

         [( 0. X), y] in E by A3, EQREL_1: 18;

        then [(x \ ( 0. X)), (x \ y)] in E by A4, Def9;

        then [x, (x \ y)] in E by BCIALG_1: 2;

        then

         A5: [(x \ y), x] in E by EQREL_1: 6;

         [( 0. X), (x \ y)] in E by A2, EQREL_1: 18;

        then [( 0. X), x] in E by A5, EQREL_1: 7;

        hence x in ( Class (E,( 0. X))) by EQREL_1: 18;

      end;

      

       A6: [( 0. X), ( 0. X)] in E by EQREL_1: 5;

      then ( 0. X) in ( Class (E,( 0. X))) by EQREL_1: 18;

      then

      reconsider Rx = ( Class (E,( 0. X))) as Ideal of X by A1, BCIALG_1:def 18;

      now

        let x be Element of Rx;

         [( 0. X), x] in E by EQREL_1: 18;

        then [(( 0. X) ` ), (x ` )] in E by A6, Def9;

        then [( 0. X), (x ` )] in E by BCIALG_1:def 5;

        hence (x ` ) in ( Class (E,( 0. X))) by EQREL_1: 18;

      end;

      hence thesis by BCIALG_1:def 19;

    end;

    theorem :: BCIALG_2:36

    

     Th36: R is Congruence of X iff R is R-congruence of X & R is L-congruence of X

    proof

      

       A1: ( field R) = the carrier of X by EQREL_1: 9;

      then

       A2: R is_reflexive_in the carrier of X by RELAT_2:def 9;

      thus R is Congruence of X implies R is R-congruence of X & R is L-congruence of X

      proof

        assume

         A3: R is Congruence of X;

        thus R is R-congruence of X

        proof

          let x,y be Element of X;

          assume

           A4: [x, y] in R;

          let u be Element of X;

           [u, u] in R by A2, RELAT_2:def 1;

          hence thesis by A3, A4, Def9;

        end;

        let x,y be Element of X;

        assume

         A5: [x, y] in R;

        let u be Element of X;

         [u, u] in R by A2, RELAT_2:def 1;

        hence thesis by A3, A5, Def9;

      end;

      assume

       A6: R is R-congruence of X & R is L-congruence of X;

      

       A7: R is_transitive_in the carrier of X by A1, RELAT_2:def 16;

      now

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

        assume [x, y] in R & [u, v] in R;

        then [(x \ u), (y \ u)] in R & [(y \ u), (y \ v)] in R by A6, Def10, Def11;

        hence [(x \ u), (y \ v)] in R by A7, RELAT_2:def 8;

      end;

      hence thesis by Def9;

    end;

    theorem :: BCIALG_2:37

    

     Th37: RI is Congruence of X

    proof

      ( field RI) = the carrier of X by EQREL_1: 9;

      then

       A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;

      now

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

        assume that

         A2: [x, y] in RI and

         A3: [u, v] in RI;

        (((y \ u) \ (y \ v)) \ (v \ u)) = ( 0. X) by BCIALG_1: 1;

        then

         A4: (((y \ u) \ (y \ v)) \ (v \ u)) in I by BCIALG_1:def 18;

        (v \ u) in I by A3, Def12;

        then

         A5: ((y \ u) \ (y \ v)) in I by A4, BCIALG_1:def 18;

        (((y \ v) \ (y \ u)) \ (u \ v)) = ( 0. X) by BCIALG_1: 1;

        then

         A6: (((y \ v) \ (y \ u)) \ (u \ v)) in I by BCIALG_1:def 18;

        (u \ v) in I by A3, Def12;

        then ((y \ v) \ (y \ u)) in I by A6, BCIALG_1:def 18;

        then

         A7: [(y \ u), (y \ v)] in RI by A5, Def12;

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

        then

         A8: (((x \ u) \ (y \ u)) \ (x \ y)) in I by BCIALG_1:def 18;

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

        then

         A9: (((y \ u) \ (x \ u)) \ (y \ x)) in I by BCIALG_1:def 18;

        (y \ x) in I by A2, Def12;

        then

         A10: ((y \ u) \ (x \ u)) in I by A9, BCIALG_1:def 18;

        (x \ y) in I by A2, Def12;

        then ((x \ u) \ (y \ u)) in I by A8, BCIALG_1:def 18;

        then [(x \ u), (y \ u)] in RI by A10, Def12;

        hence [(x \ u), (y \ v)] in RI by A1, A7, RELAT_2:def 8;

      end;

      hence thesis by Def9;

    end;

    definition

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

      :: original: I-congruence

      redefine

      mode I-congruence of X,I -> Congruence of X ;

      coherence by Th37;

    end

    theorem :: BCIALG_2:38

    

     Th38: ( Class (RI,( 0. X))) c= I

    proof

      let x be object;

      assume

       A1: x in ( Class (RI,( 0. X)));

      then

      consider y be object such that

       A2: [y, x] in RI and

       A3: y in {( 0. X)} by RELAT_1:def 13;

      reconsider x as Element of X by A1;

      reconsider y as Element of X by A3, TARSKI:def 1;

      y = ( 0. X) by A3, TARSKI:def 1;

      then (x \ ( 0. X)) in I by A2, Def12;

      hence thesis by BCIALG_1: 2;

    end;

    theorem :: BCIALG_2:39

    I is closed iff I = ( Class (RI,( 0. X)))

    proof

      thus I is closed implies I = ( Class (RI,( 0. X)))

      proof

        assume

         A1: I is closed;

        thus I c= ( Class (RI,( 0. X)))

        proof

          let x be object;

          assume

           A2: x in I;

          then

          reconsider x as Element of I;

          

           A3: (x \ ( 0. X)) in I by A2, BCIALG_1: 2;

          (x ` ) in I by A1;

          then ( 0. X) in {( 0. X)} & [( 0. X), x] in RI by A3, Def12, TARSKI:def 1;

          hence thesis by RELAT_1:def 13;

        end;

        thus thesis by Th38;

      end;

      assume

       A4: I = ( Class (RI,( 0. X)));

      now

        let x be Element of I;

        ex y be object st [y, x] in RI & y in {( 0. X)} by A4, RELAT_1:def 13;

        then [( 0. X), x] in RI by TARSKI:def 1;

        hence (x ` ) in I by Def12;

      end;

      hence thesis;

    end;

    theorem :: BCIALG_2:40

    

     Th40: [x, y] in E implies (x \ y) in ( Class (E,( 0. X))) & (y \ x) in ( Class (E,( 0. X)))

    proof

      assume

       A1: [x, y] in E;

      

       A2: ( field E) = the carrier of X by EQREL_1: 9;

      then

       A3: E is_reflexive_in the carrier of X by RELAT_2:def 9;

      then

       A4: [y, y] in E by RELAT_2:def 1;

      E is_symmetric_in the carrier of X by A2, RELAT_2:def 11;

      then [y, x] in E by A1, RELAT_2:def 3;

      then [(y \ y), (x \ y)] in E by A4, Def9;

      then

       A5: [( 0. X), (x \ y)] in E by BCIALG_1:def 5;

       [x, x] in E by A3, RELAT_2:def 1;

      then [(x \ x), (y \ x)] in E by A1, Def9;

      then ( 0. X) in {( 0. X)} & [( 0. X), (y \ x)] in E by BCIALG_1:def 5, TARSKI:def 1;

      hence thesis by A5, RELAT_1:def 13;

    end;

    theorem :: BCIALG_2:41

    for A,I be Ideal of X, IA be I-congruence of X, A, II be I-congruence of X, I st ( Class (IA,( 0. X))) = ( Class (II,( 0. X))) holds IA = II

    proof

      let A,I be Ideal of X, IA be I-congruence of X, A, II be I-congruence of X, I;

      assume

       A1: ( Class (IA,( 0. X))) = ( Class (II,( 0. X)));

      let xx,yy be object;

      thus [xx, yy] in IA implies [xx, yy] in II

      proof

        assume

         A2: [xx, yy] in IA;

        then

        consider x,y be object such that

         A3: [xx, yy] = [x, y] and

         A4: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A4;

        (x \ y) in (II .: {( 0. X)}) by A1, A2, A3, Th40;

        then ex z be object st [z, (x \ y)] in II & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (x \ y)] in II by TARSKI:def 1;

        then ((x \ y) \ ( 0. X)) in I by Def12;

        then

         A5: (x \ y) in I by BCIALG_1: 2;

        (y \ x) in (II .: {( 0. X)}) by A1, A2, A3, Th40;

        then ex z be object st [z, (y \ x)] in II & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (y \ x)] in II by TARSKI:def 1;

        then ((y \ x) \ ( 0. X)) in I by Def12;

        then (y \ x) in I by BCIALG_1: 2;

        hence thesis by A3, A5, Def12;

      end;

      thus [xx, yy] in II implies [xx, yy] in IA

      proof

        assume

         A6: [xx, yy] in II;

        then

        consider x,y be object such that

         A7: [xx, yy] = [x, y] and

         A8: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A8;

        (x \ y) in (IA .: {( 0. X)}) by A1, A6, A7, Th40;

        then ex z be object st [z, (x \ y)] in IA & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (x \ y)] in IA by TARSKI:def 1;

        then ((x \ y) \ ( 0. X)) in A by Def12;

        then

         A9: (x \ y) in A by BCIALG_1: 2;

        (y \ x) in (IA .: {( 0. X)}) by A1, A6, A7, Th40;

        then ex z be object st [z, (y \ x)] in IA & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (y \ x)] in IA by TARSKI:def 1;

        then ((y \ x) \ ( 0. X)) in A by Def12;

        then (y \ x) in A by BCIALG_1: 2;

        hence thesis by A7, A9, Def12;

      end;

    end;

    theorem :: BCIALG_2:42

    

     Th42: [x, y] in E & u in ( Class (E,( 0. X))) implies [x, ((y,u) to_power k)] in E

    proof

      assume that

       A1: [x, y] in E and

       A2: u in ( Class (E,( 0. X)));

      defpred P[ Nat] means [x, ((y,u) to_power $1)] in E;

      ex z be object st [z, u] in E & z in {( 0. X)} by A2, RELAT_1:def 13;

      then

       A3: [( 0. X), u] in E by TARSKI:def 1;

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume [x, ((y,u) to_power k)] in E;

        then [(x \ ( 0. X)), (((y,u) to_power k) \ u)] in E by A3, Def9;

        then [x, (((y,u) to_power k) \ u)] in E by BCIALG_1: 2;

        hence thesis by Th4;

      end;

      

       A5: P[ 0 ] by A1, Th1;

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

      hence thesis;

    end;

    theorem :: BCIALG_2:43

    (for X, x, y holds ex i, j, m, n st ((((x,(x \ y)) to_power i),(y \ x)) to_power j) = ((((y,(y \ x)) to_power m),(x \ y)) to_power n)) implies for E, I st I = ( Class (E,( 0. X))) holds E is I-congruence of X, I

    proof

      assume

       A1: for X, x, y holds ex i, j, m, n st ((((x,(x \ y)) to_power i),(y \ x)) to_power j) = ((((y,(y \ x)) to_power m),(x \ y)) to_power n);

      let E, I;

      assume

       A2: I = ( Class (E,( 0. X)));

      now

        let x,y be Element of X;

        (x \ y) in I & (y \ x) in I implies [x, y] in E

        proof

          assume that

           A3: (x \ y) in I and

           A4: (y \ x) in I;

          ex z be object st [z, (y \ x)] in E & z in {( 0. X)} by A2, A4, RELAT_1:def 13;

          then

           A5: [( 0. X), (y \ x)] in E by TARSKI:def 1;

          ex z be object st [z, (x \ y)] in E & z in {( 0. X)} by A2, A3, RELAT_1:def 13;

          then

           A6: [( 0. X), (x \ y)] in E by TARSKI:def 1;

          consider i,j,m,n be Nat such that

           A7: ((((x,(x \ y)) to_power i),(y \ x)) to_power j) = ((((y,(y \ x)) to_power m),(x \ y)) to_power n) by A1;

          

           A8: ( field E) = the carrier of X by EQREL_1: 9;

          

           A9: E is_reflexive_in ( field E) by RELAT_2:def 9;

          then [x, x] in E by A8, RELAT_2:def 1;

          then

           A10: [x, ((x,(x \ y)) to_power i)] in E by A2, A3, Th42;

          

           A11: [x, ((((x,(x \ y)) to_power i),(y \ x)) to_power j)] in E

          proof

            defpred P[ Nat] means [x, ((((x,(x \ y)) to_power i),(y \ x)) to_power $1)] in E;

            

             A12: for k be Nat st P[k] holds P[(k + 1)]

            proof

              let k be Nat;

              assume [x, ((((x,(x \ y)) to_power i),(y \ x)) to_power k)] in E;

              then [(x \ ( 0. X)), (((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by A5, Def9;

              then [x, (((((x,(x \ y)) to_power i),(y \ x)) to_power k) \ (y \ x))] in E by BCIALG_1: 2;

              hence thesis by Th4;

            end;

            

             A13: P[ 0 ] by A10, Th1;

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

            hence thesis;

          end;

           [y, y] in E by A8, A9, RELAT_2:def 1;

          then

           A14: [y, ((y,(y \ x)) to_power m)] in E by A2, A4, Th42;

          

           A15: [y, ((((y,(y \ x)) to_power m),(x \ y)) to_power n)] in E

          proof

            defpred P[ Nat] means [y, ((((y,(y \ x)) to_power m),(x \ y)) to_power $1)] in E;

            

             A16: for k be Nat st P[k] holds P[(k + 1)]

            proof

              let k be Nat;

              assume [y, ((((y,(y \ x)) to_power m),(x \ y)) to_power k)] in E;

              then [(y \ ( 0. X)), (((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by A6, Def9;

              then [y, (((((y,(y \ x)) to_power m),(x \ y)) to_power k) \ (x \ y))] in E by BCIALG_1: 2;

              hence thesis by Th4;

            end;

            

             A17: P[ 0 ] by A14, Th1;

            for n holds P[n] from NAT_1:sch 2( A17, A16);

            hence thesis;

          end;

          E is_symmetric_in ( field E) by RELAT_2:def 11;

          then E is_transitive_in ( field E) & [((((x,(x \ y)) to_power i),(y \ x)) to_power j), y] in E by A7, A8, A15, RELAT_2:def 3, RELAT_2:def 16;

          hence thesis by A8, A11, RELAT_2:def 8;

        end;

        hence [x, y] in E iff (x \ y) in I & (y \ x) in I by A2, Th40;

      end;

      hence thesis by Def12;

    end;

    theorem :: BCIALG_2:44

    ( IConSet X) c= ( ConSet X)

    proof

      let x be object;

      assume x in ( IConSet X);

      then ex I be Ideal of X st x is I-congruence of X, I by Def13;

      hence thesis;

    end;

    theorem :: BCIALG_2:45

    

     Th45: ( ConSet X) c= ( LConSet X)

    proof

      let x be object;

      assume x in ( ConSet X);

      then ex R be Congruence of X st x = R;

      then x is L-congruence of X by Th36;

      hence thesis;

    end;

    theorem :: BCIALG_2:46

    

     Th46: ( ConSet X) c= ( RConSet X)

    proof

      let x be object;

      assume x in ( ConSet X);

      then ex R be Congruence of X st x = R;

      then x is R-congruence of X by Th36;

      hence thesis;

    end;

    theorem :: BCIALG_2:47

    ( ConSet X) = (( LConSet X) /\ ( RConSet X))

    proof

      ( ConSet X) c= ( LConSet X) & ( ConSet X) c= ( RConSet X) by Th45, Th46;

      hence ( ConSet X) c= (( LConSet X) /\ ( RConSet X)) by XBOOLE_1: 19;

      thus (( LConSet X) /\ ( RConSet X)) c= ( ConSet X)

      proof

        let x be object;

        assume

         A1: x in (( LConSet X) /\ ( RConSet X));

        then x in ( RConSet X) by XBOOLE_0:def 4;

        then

         A2: ex R be R-congruence of X st x = R;

        x in ( LConSet X) by A1, XBOOLE_0:def 4;

        then ex L be L-congruence of X st x = L;

        then x is Congruence of X by A2, Th36;

        hence thesis;

      end;

    end;

    theorem :: BCIALG_2:48

    (for LC holds LC is I-congruence of X, I) implies E = RI

    proof

      assume

       A1: for LC holds LC is I-congruence of X, I;

      let x1,y1 be object;

      E is L-congruence of X by Th36;

      then

       A2: E is I-congruence of X, I by A1;

      thus [x1, y1] in E implies [x1, y1] in RI

      proof

        assume

         A3: [x1, y1] in E;

        then

        consider x,y be object such that

         A4: [x1, y1] = [x, y] and

         A5: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A5;

        (y \ x) in ( Class (E,( 0. X))) by A3, A4, Th40;

        then ex z be object st [z, (y \ x)] in E & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (y \ x)] in E by TARSKI:def 1;

        then ((y \ x) \ ( 0. X)) in I by A2, Def12;

        then

         A6: (y \ x) in I by BCIALG_1: 2;

        (x \ y) in ( Class (E,( 0. X))) by A3, A4, Th40;

        then ex z be object st [z, (x \ y)] in E & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (x \ y)] in E by TARSKI:def 1;

        then ((x \ y) \ ( 0. X)) in I by A2, Def12;

        then (x \ y) in I by BCIALG_1: 2;

        hence thesis by A4, A6, Def12;

      end;

      thus [x1, y1] in RI implies [x1, y1] in E

      proof

        assume

         A7: [x1, y1] in RI;

        then

        consider x,y be object such that

         A8: [x1, y1] = [x, y] and

         A9: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A9;

        (x \ y) in I & (y \ x) in I by A7, A8, Def12;

        hence thesis by A2, A8, Def12;

      end;

    end;

    theorem :: BCIALG_2:49

    (for RC holds RC is I-congruence of X, I) implies E = RI

    proof

      assume

       A1: for RC holds RC is I-congruence of X, I;

      let x1,y1 be object;

      E is R-congruence of X by Th36;

      then

       A2: E is I-congruence of X, I by A1;

      thus [x1, y1] in E implies [x1, y1] in RI

      proof

        assume

         A3: [x1, y1] in E;

        then

        consider x,y be object such that

         A4: [x1, y1] = [x, y] and

         A5: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A5;

        (y \ x) in ( Class (E,( 0. X))) by A3, A4, Th40;

        then ex z be object st [z, (y \ x)] in E & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (y \ x)] in E by TARSKI:def 1;

        then ((y \ x) \ ( 0. X)) in I by A2, Def12;

        then

         A6: (y \ x) in I by BCIALG_1: 2;

        (x \ y) in ( Class (E,( 0. X))) by A3, A4, Th40;

        then ex z be object st [z, (x \ y)] in E & z in {( 0. X)} by RELAT_1:def 13;

        then [( 0. X), (x \ y)] in E by TARSKI:def 1;

        then ((x \ y) \ ( 0. X)) in I by A2, Def12;

        then (x \ y) in I by BCIALG_1: 2;

        hence thesis by A4, A6, Def12;

      end;

      thus [x1, y1] in RI implies [x1, y1] in E

      proof

        assume

         A7: [x1, y1] in RI;

        then

        consider x,y be object such that

         A8: [x1, y1] = [x, y] and

         A9: x in the carrier of X & y in the carrier of X by RELSET_1: 2;

        reconsider x, y as Element of X by A9;

        (x \ y) in I & (y \ x) in I by A7, A8, Def12;

        hence thesis by A2, A8, Def12;

      end;

    end;

    theorem :: BCIALG_2:50

    ( Class (LC,( 0. X))) is closed Ideal of X

    proof

       A1:

      now

        let x,y be Element of X;

        assume that

         A2: (x \ y) in ( Class (LC,( 0. X))) and

         A3: y in ( Class (LC,( 0. X)));

         [( 0. X), y] in LC by A3, EQREL_1: 18;

        then [(x \ ( 0. X)), (x \ y)] in LC by Def10;

        then [x, (x \ y)] in LC by BCIALG_1: 2;

        then

         A4: [(x \ y), x] in LC by EQREL_1: 6;

         [( 0. X), (x \ y)] in LC by A2, EQREL_1: 18;

        then [( 0. X), x] in LC by A4, EQREL_1: 7;

        hence x in ( Class (LC,( 0. X))) by EQREL_1: 18;

      end;

       [( 0. X), ( 0. X)] in LC by EQREL_1: 5;

      then ( 0. X) in ( Class (LC,( 0. X))) by EQREL_1: 18;

      then

      reconsider Rx = ( Class (LC,( 0. X))) as Ideal of X by A1, BCIALG_1:def 18;

      now

        let x be Element of Rx;

         [( 0. X), x] in LC by EQREL_1: 18;

        then [(( 0. X) ` ), (x ` )] in LC by Def10;

        then [( 0. X), (x ` )] in LC by BCIALG_1:def 5;

        hence (x ` ) in ( Class (LC,( 0. X))) by EQREL_1: 18;

      end;

      hence thesis by BCIALG_1:def 19;

    end;

    reserve E for Congruence of X;

    reserve RI for I-congruence of X, I;

    registration

      let X, E;

      cluster ( Class E) -> non empty;

      coherence

      proof

        ( Class (E,( 0. X))) in ( Class E) by EQREL_1:def 3;

        hence thesis;

      end;

    end

    definition

      let X, E;

      :: BCIALG_2:def17

      func EqClaOp E -> BinOp of ( Class E) means

      : Def17: for W1,W2 be Element of ( Class E) holds for x, y st W1 = ( Class (E,x)) & W2 = ( Class (E,y)) holds (it . (W1,W2)) = ( Class (E,(x \ y)));

      existence

      proof

        defpred P[ Element of ( Class E), Element of ( Class E), set] means for x, y st $1 = ( Class (E,x)) & $2 = ( Class (E,y)) holds $3 = ( Class (E,(x \ y)));

        

         A1: for W1,W2 be Element of ( Class E) holds ex V be Element of ( Class E) st P[W1, W2, V]

        proof

          let W1,W2 be Element of ( Class E);

          consider x1 be object such that

           A2: x1 in the carrier of X and

           A3: W1 = ( Class (E,x1)) by EQREL_1:def 3;

          consider y1 be object such that

           A4: y1 in the carrier of X and

           A5: W2 = ( Class (E,y1)) by EQREL_1:def 3;

          reconsider x1, y1 as Element of X by A2, A4;

          reconsider C = ( Class (E,(x1 \ y1))) as Element of ( Class E) by EQREL_1:def 3;

          take C;

          now

            let x, y;

            assume that

             A6: W1 = ( Class (E,x)) and

             A7: W2 = ( Class (E,y));

            y in ( Class (E,y1)) by A5, A7, EQREL_1: 23;

            then

             A8: [y1, y] in E by EQREL_1: 18;

            x in ( Class (E,x1)) by A3, A6, EQREL_1: 23;

            then [x1, x] in E by EQREL_1: 18;

            then [(x1 \ y1), (x \ y)] in E by A8, Def9;

            then (x \ y) in ( Class (E,(x1 \ y1))) by EQREL_1: 18;

            hence C = ( Class (E,(x \ y))) by EQREL_1: 23;

          end;

          hence thesis;

        end;

        thus ex B be BinOp of ( Class E) st for W1,W2 be Element of ( Class E) holds P[W1, W2, (B . (W1,W2))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Class E);

        assume

         A9: for W1,W2 be Element of ( Class E) holds for x, y st W1 = ( Class (E,x)) & W2 = ( Class (E,y)) holds (o1 . (W1,W2)) = ( Class (E,(x \ y)));

        assume

         A10: for W1,W2 be Element of ( Class E) holds for x, y st W1 = ( Class (E,x)) & W2 = ( Class (E,y)) holds (o2 . (W1,W2)) = ( Class (E,(x \ y)));

        now

          let W1,W2 be Element of ( Class E);

          consider x be object such that

           A11: x in the carrier of X and

           A12: W1 = ( Class (E,x)) by EQREL_1:def 3;

          consider y be object such that

           A13: y in the carrier of X and

           A14: W2 = ( Class (E,y)) by EQREL_1:def 3;

          reconsider x, y as Element of X by A11, A13;

          (o1 . (W1,W2)) = ( Class (E,(x \ y))) by A9, A12, A14;

          hence (o1 . (W1,W2)) = (o2 . (W1,W2)) by A10, A12, A14;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let X, E;

      :: BCIALG_2:def18

      func zeroEqC (E) -> Element of ( Class E) equals ( Class (E,( 0. X)));

      coherence by EQREL_1:def 3;

    end

    definition

      let X, E;

      :: BCIALG_2:def19

      func X ./. E -> BCIStr_0 equals BCIStr_0 (# ( Class E), ( EqClaOp E), ( zeroEqC E) #);

      coherence ;

    end

    registration

      let X;

      let E be Congruence of X;

      cluster (X ./. E) -> non empty;

      coherence ;

    end

    reserve W1,W2 for Element of ( Class E);

    definition

      let X, E, W1, W2;

      :: BCIALG_2:def20

      func W1 \ W2 -> Element of ( Class E) equals (( EqClaOp E) . (W1,W2));

      coherence ;

    end

    theorem :: BCIALG_2:51

    

     Th51: (X ./. RI) is BCI-algebra

    proof

      reconsider IT = (X ./. RI) as non empty BCIStr_0;

       A1:

      now

        let w1,w2,w3 be Element of IT;

        w1 in the carrier of IT;

        then

        consider x1 be object such that

         A2: x1 in the carrier of X and

         A3: w1 = ( Class (RI,x1)) by EQREL_1:def 3;

        w3 in the carrier of IT;

        then

        consider z1 be object such that

         A4: z1 in the carrier of X and

         A5: w3 = ( Class (RI,z1)) by EQREL_1:def 3;

        w2 in the carrier of IT;

        then

        consider y1 be object such that

         A6: y1 in the carrier of X and

         A7: w2 = ( Class (RI,y1)) by EQREL_1:def 3;

        reconsider x1, y1, z1 as Element of X by A2, A6, A4;

        

         A8: (w3 \ w2) = ( Class (RI,(z1 \ y1))) by A7, A5, Def17;

        (w1 \ w2) = ( Class (RI,(x1 \ y1))) by A3, A7, Def17;

        then

         A9: ((w1 \ w2) \ (w3 \ w2)) = ( Class (RI,((x1 \ y1) \ (z1 \ y1)))) by A8, Def17;

        (w1 \ w3) = ( Class (RI,(x1 \ z1))) by A3, A5, Def17;

        then (((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3)) = ( Class (RI,(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1)))) by A9, Def17;

        hence (((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3)) = ( 0. IT) by BCIALG_1:def 3;

      end;

       A10:

      now

        let w1,w2,w3 be Element of IT;

        w1 in the carrier of IT;

        then

        consider x1 be object such that

         A11: x1 in the carrier of X and

         A12: w1 = ( Class (RI,x1)) by EQREL_1:def 3;

        w2 in the carrier of IT;

        then

        consider y1 be object such that

         A13: y1 in the carrier of X and

         A14: w2 = ( Class (RI,y1)) by EQREL_1:def 3;

        w3 in the carrier of IT;

        then

        consider z1 be object such that

         A15: z1 in the carrier of X and

         A16: w3 = ( Class (RI,z1)) by EQREL_1:def 3;

        reconsider x1, y1, z1 as Element of X by A11, A13, A15;

        (w1 \ w3) = ( Class (RI,(x1 \ z1))) by A12, A16, Def17;

        then

         A17: ((w1 \ w3) \ w2) = ( Class (RI,((x1 \ z1) \ y1))) by A14, Def17;

        (w1 \ w2) = ( Class (RI,(x1 \ y1))) by A12, A14, Def17;

        then ((w1 \ w2) \ w3) = ( Class (RI,((x1 \ y1) \ z1))) by A16, Def17;

        then (((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2)) = ( Class (RI,(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1)))) by A17, Def17;

        hence (((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2)) = ( 0. IT) by BCIALG_1:def 4;

      end;

       A18:

      now

        let w1,w2 be Element of IT;

        assume that

         A19: (w1 \ w2) = ( 0. IT) and

         A20: (w2 \ w1) = ( 0. IT);

        w1 in the carrier of IT;

        then

        consider x1 be object such that

         A21: x1 in the carrier of X and

         A22: w1 = ( Class (RI,x1)) by EQREL_1:def 3;

        w2 in the carrier of IT;

        then

        consider y1 be object such that

         A23: y1 in the carrier of X and

         A24: w2 = ( Class (RI,y1)) by EQREL_1:def 3;

        reconsider x1, y1 as Element of X by A21, A23;

        (w2 \ w1) = ( Class (RI,(y1 \ x1))) by A22, A24, Def17;

        then ( 0. X) in ( Class (RI,(y1 \ x1))) by A20, EQREL_1: 23;

        then [(y1 \ x1), ( 0. X)] in RI by EQREL_1: 18;

        then ((y1 \ x1) \ ( 0. X)) in I by Def12;

        then

         A25: (y1 \ x1) in I by BCIALG_1: 2;

        (w1 \ w2) = ( Class (RI,(x1 \ y1))) by A22, A24, Def17;

        then ( 0. X) in ( Class (RI,(x1 \ y1))) by A19, EQREL_1: 23;

        then [(x1 \ y1), ( 0. X)] in RI by EQREL_1: 18;

        then ((x1 \ y1) \ ( 0. X)) in I by Def12;

        then (x1 \ y1) in I by BCIALG_1: 2;

        then [x1, y1] in RI by A25, Def12;

        hence w1 = w2 by A22, A24, EQREL_1: 35;

      end;

      now

        let w1 be Element of IT;

        w1 in the carrier of IT;

        then

        consider x1 be object such that

         A26: x1 in the carrier of X and

         A27: w1 = ( Class (RI,x1)) by EQREL_1:def 3;

        reconsider x1 as Element of X by A26;

        (w1 \ w1) = ( Class (RI,(x1 \ x1))) by A27, Def17;

        hence (w1 \ w1) = ( 0. IT) by BCIALG_1:def 5;

      end;

      hence thesis by A1, A10, A18, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7;

    end;

    registration

      let X, I, RI;

      cluster (X ./. RI) -> strict being_B being_C being_I being_BCI-4;

      coherence by Th51;

    end

    theorem :: BCIALG_2:52

    for X, I st I = ( BCK-part X) holds for RI be I-congruence of X, I holds (X ./. RI) is p-Semisimple BCI-algebra

    proof

      let X, I;

      assume

       A1: I = ( BCK-part X);

      let RI be I-congruence of X, I;

      set IT = (X ./. RI);

      for w1 be Element of IT holds ((w1 ` ) ` ) = w1

      proof

        let w1 be Element of IT;

        w1 in the carrier of IT;

        then

        consider x1 be object such that

         A2: x1 in the carrier of X and

         A3: w1 = ( Class (RI,x1)) by EQREL_1:def 3;

        reconsider x1 as Element of X by A2;

        (w1 ` ) = ( Class (RI,(x1 ` ))) by A3, Def17;

        then

         A4: ((w1 ` ) ` ) = ( Class (RI,((x1 ` ) ` ))) by Def17;

        (x1 \ ((x1 ` ) ` )) is positive Element of X by Th28;

        then ( 0. X) <= (x1 \ ((x1 ` ) ` )) by Def2;

        then

         A5: (x1 \ ((x1 ` ) ` )) in I by A1;

        ( 0. X) in I by BCIALG_1:def 18;

        then (((x1 ` ) ` ) \ x1) in I by BCIALG_1: 1;

        then [((x1 ` ) ` ), x1] in RI by A5, Def12;

        hence thesis by A3, A4, EQREL_1: 35;

      end;

      hence thesis by BCIALG_1: 54;

    end;