:: BCIALG_3 semantic presentation

begin

definition
let IT be ( ( non empty ) ( non empty ) BCIStr_0 ) ;
attr IT is commutative means :: BCIALG_3:def 1
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster BCI-EXAMPLE : ( ( ) ( non empty V42() V43() V48(1 : ( ( ) ( ) set ) ) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative ) BCIStr_0 ) -> commutative ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative for ( ( ) ( ) BCIStr_0 ) ;
end;

theorem :: BCIALG_3:1
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:2
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:3
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:4
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:5
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:6
for X being ( ( non empty ) ( non empty ) BCIStr_0 ) holds
( X : ( ( non empty ) ( non empty ) BCIStr_0 ) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((0. X : ( ( non empty ) ( non empty ) BCIStr_0 ) ) : ( ( ) ( V44(b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) ) ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: BCIALG_3:7
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_3:8
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
for x, y, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
(a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_3:9
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( V44(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:10
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:11
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
for x, y, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
(a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr a is being_greatest means :: BCIALG_3:def 2
 for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V44(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;
attr a is being_positive means :: BCIALG_3:def 3
(0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( V44(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ a : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V44(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;
end;

begin

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;
attr IT is BCI-commutative means :: BCIALG_3:def 4
 for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V44(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;
attr IT is BCI-weakly-commutative means :: BCIALG_3:def 5
 for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ ((0. IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( V44(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster BCI-EXAMPLE : ( ( ) ( non empty V42() V43() V48(1 : ( ( ) ( ) set ) ) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative commutative ) BCIStr_0 ) -> BCI-commutative BCI-weakly-commutative ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative for ( ( ) ( ) BCIStr_0 ) ;
end;

theorem :: BCIALG_3:12
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) st ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;

theorem :: BCIALG_3:13
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is p-Semisimple holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative & X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-weakly-commutative ) ;

theorem :: BCIALG_3:14
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 BCI-commutative ) ( non empty being_B being_C being_I being_BCI-4 BCI-commutative ) BCI-algebra) & X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 BCI-weakly-commutative ) ( non empty being_B being_C being_I being_BCI-4 BCI-weakly-commutative ) BCI-algebra) ) ;

theorem :: BCIALG_3:15
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 BCI-weakly-commutative ) ( non empty being_B being_C being_I being_BCI-4 BCI-weakly-commutative ) BCI-algebra) holds
X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is BCI-commutative ;

theorem :: BCIALG_3:16
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:17
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = (0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( V44(b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:18
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative iff for a being ( ( ) ( ) Element of AtomSet X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) )
for x, y being ( ( ) ( ) Element of BranchV a : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) holds x : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) \ (x : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) \ y : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) \ (y : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) \ x : ( ( ) ( ) Element of BranchV b2 : ( ( ) ( ) Element of AtomSet b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty ) Element of K19( the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:19
for X being ( ( non empty ) ( non empty ) BCIStr_0 ) holds
( X : ( ( non empty ) ( non empty ) BCIStr_0 ) is ( ( non empty being_B being_C being_I being_BCI-4 BCI-commutative ) ( non empty being_B being_C being_I being_BCI-4 BCI-commutative ) BCI-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( V44(b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) ) ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (0. X : ( ( non empty ) ( non empty ) BCIStr_0 ) ) : ( ( ) ( V44(b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) ) ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: BCIALG_3:20
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:21
for X being ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) is BCI-commutative iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) : ( ( ) ( non empty ) set ) ) ) ;

begin

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;
attr IT is bounded means :: BCIALG_3:def 6
 ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest ;
end;

registration
cluster BCI-EXAMPLE : ( ( ) ( non empty V42() V43() V48(1 : ( ( ) ( ) set ) ) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative commutative BCI-commutative BCI-weakly-commutative ) BCIStr_0 ) -> bounded ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded for ( ( ) ( ) BCIStr_0 ) ;
end;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) ;
attr IT is involutory means :: BCIALG_3:def 7
 for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: BCIALG_3:22
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is involutory iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:23
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is involutory iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:24
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is involutory iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) holds
y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr a is being_Iseki means :: BCIALG_3:def 8
 for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ a : ( ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = 0. IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V44(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) & a : ( ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = a : ( ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;
attr IT is Iseki_extension means :: BCIALG_3:def 9
 ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_Iseki ;
end;

registration
cluster BCI-EXAMPLE : ( ( ) ( non empty V42() V43() V48(1 : ( ( ) ( ) set ) ) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative commutative BCI-commutative BCI-weakly-commutative bounded ) BCIStr_0 ) -> Iseki_extension ;
end;

definition
let X be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;
mode Commutative-Ideal of X -> ( ( non empty ) ( non empty ) Subset of ) means :: BCIALG_3:def 10
( 0. X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( V44(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) in it : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) in it : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in it : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) in it : ( ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) ( V6() V18(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) ) Element of K19(K20(K20(X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ,X : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

theorem :: BCIALG_3:25
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra)
for IT being ( ( non empty ) ( non empty ) Subset of ) st IT : ( ( non empty ) ( non empty ) Subset of ) is ( ( ) ( non empty ) Commutative-Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) in IT : ( ( non empty ) ( non empty ) Subset of ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) in IT : ( ( non empty ) ( non empty ) Subset of ) ;

theorem :: BCIALG_3:26
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra)
for IT being ( ( non empty ) ( non empty ) Subset of )
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) st IT : ( ( non empty ) ( non empty ) Subset of ) is ( ( ) ( non empty ) Commutative-Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) holds
IT : ( ( non empty ) ( non empty ) Subset of ) is ( ( ) ( non empty ) Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) ;

theorem :: BCIALG_3:27
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra)
for IT being ( ( non empty ) ( non empty ) Subset of ) st IT : ( ( non empty ) ( non empty ) Subset of ) is ( ( ) ( non empty ) Commutative-Ideal of X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) in IT : ( ( non empty ) ( non empty ) Subset of ) holds
(y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) in IT : ( ( non empty ) ( non empty ) Subset of ) ;

begin

definition
let IT be ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ;
attr IT is BCK-positive-implicative means :: BCIALG_3:def 11
 for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ;
attr IT is BCK-implicative means :: BCIALG_3:def 12
 for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of IT : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster BCI-EXAMPLE : ( ( ) ( non empty V42() V43() V48(1 : ( ( ) ( ) set ) ) strict being_B being_C being_I being_BCI-4 being_BCK-5 associative positive-implicative weakly-positive-implicative V67() weakly-implicative p-Semisimple alternative commutative BCI-commutative BCI-weakly-commutative bounded Iseki_extension ) BCIStr_0 ) -> BCK-positive-implicative BCK-implicative ;
end;

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative for ( ( ) ( ) BCIStr_0 ) ;
end;

theorem :: BCIALG_3:28
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:29
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:30
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:31
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:32
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:33
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:34
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff ( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative ) BCK-algebra) & X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-positive-implicative ) BCK-algebra) ) ) ;

theorem :: BCIALG_3:35
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:36
for X being ( ( non empty ) ( non empty ) BCIStr_0 ) holds
( X : ( ( non empty ) ( non empty ) BCIStr_0 ) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((0. X : ( ( non empty ) ( non empty ) BCIStr_0 ) ) : ( ( ) ( V44(b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) ) ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) = ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty ) ( non empty ) BCIStr_0 ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: BCIALG_3:37
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is BCK-implicative iff ( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is involutory & X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 bounded ) BCK-algebra) is BCK-positive-implicative ) ) ;

theorem :: BCIALG_3:38
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( V44(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) ) ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:39
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:40
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:41
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:42
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) is ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 BCK-implicative ) BCK-algebra) iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:43
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = 0. X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( V44(b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) ) ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:44
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:45
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:46
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ ((a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:47
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_3:48
for X being ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is being_greatest holds
( X : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) is BCK-implicative iff for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) \ (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the U1 of b1 : ( ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) ( non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded ) BCK-algebra) : ( ( ) ( non empty ) set ) ) ) ;