BCIALG_2

:: BCIALG_2 semantic presentation

begin

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 x, y be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let n be ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

func (x,y) to_power n -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: BCIALG_2:def 1
ex f being ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ) Function of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) st
( it : ( ( Function-like ) ( Relation-like X : ( ( ) ( ) BCIStr_0 ) -defined x : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like ) Element of bool [:X : ( ( ) ( ) BCIStr_0 ) ,x : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of 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 ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) Function of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) . n : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) & f : ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of 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 ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) Function of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) . 0 : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) = x : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & ( for j being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st j : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) < n : ( ( ) ( ) set ) holds
f : ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of 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 ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) Function of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) . (j : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) = (f : ( ( Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of 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 ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) ) Function of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of 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 ) set ) ) . j : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) \ y : ( ( ) ( ) Element of X : ( ( ) ( ) BCIStr_0 ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) ) );

end;

theorem :: BCIALG_2:1

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power 0 : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:2

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:3

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power 2 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:4

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power (n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:5

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (x : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power (n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:6

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)
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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_2:7

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)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:8

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (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 carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:9

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:10

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n, m being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power (n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:11

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)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n, m being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n, m being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power (n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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_2:14

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for m, n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power (m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) + n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:15

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for m, n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds (((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power (m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for m, n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st ((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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
((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power (m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) * n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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_2: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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) holds
(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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(b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:19

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)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= (y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x, y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
(z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2: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)
for x, z, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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_2:22

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( 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 carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

notation

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 ) ) ;
synonym minimal a for atom ;

end;

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 positive means :: BCIALG_2:def 2
0. X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( V44(X : ( ( ) ( ) BCIStr_0 ) ) ) Element of the carrier of X : ( ( ) ( ) BCIStr_0 ) : ( ( ) ( ) set ) ) <= a : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

attr a is least means :: BCIALG_2:def 3
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds a : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

attr a is maximal means :: BCIALG_2:def 4
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st a : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

attr a is greatest means :: BCIALG_2:def 5
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) ( Relation-like [:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) BCIStr_0 ) -valued Function-like V18([:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) ) ) Element of bool [:[:X : ( ( ) ( ) BCIStr_0 ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) BCIStr_0 ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

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) ;

cluster positive for ( ( ) ( ) Element of the carrier 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;

registration

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) ;

cluster 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 carrier 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 ) ) -> minimal positive ;

end;

theorem :: BCIALG_2:23

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)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is minimal 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 carrier of b₁ : ( ( 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 ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) \ (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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_2:24

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) is minimal iff for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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_2:25

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) is minimal iff for y, z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) \ z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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_2:26

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 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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive ) Element of the carrier of b₁ : ( ( 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 ) ) is maximal holds
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is minimal ;

theorem :: BCIALG_2:27

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 x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is greatest holds
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is positive ;

theorem :: BCIALG_2:28

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ ((x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) is ( ( positive ) ( positive ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: BCIALG_2:29

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)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is minimal iff (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 carrier of b₁ : ( ( 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 ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_2:30

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)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is minimal iff ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ) ;

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 x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

attr x is nilpotent means :: BCIALG_2:def 6
ex k being ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st ((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 ) ) minimal positive ) Element of the carrier 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 ) ) ,x : ( ( non empty ) ( non empty ) set ) ) to_power k : ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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 ) ) minimal positive ) Element of the carrier 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;

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) ;

attr X is nilpotent means :: BCIALG_2:def 7
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is nilpotent ;

end;

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 x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is nilpotent ;

func ord x -> ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) means :: BCIALG_2:def 8
( ((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 ) ) minimal positive ) Element of the carrier 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 ) ) ,x : ( ( non empty ) ( non empty ) set ) ) to_power it : ( ( ) ( ) Element 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 ) ) : ( ( ) ( ) Element of ( ( ) ( 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 ) ) minimal positive ) Element of the carrier 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 ) ) & ( for m being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st ((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 ) ) minimal positive ) Element of the carrier 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 ) ) ,x : ( ( non empty ) ( non empty ) set ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( 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 ) ) minimal positive ) Element of the carrier 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 ) ) & m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) <> 0 : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds
it : ( ( ) ( ) Element 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 ) ) <= m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) );

end;

registration

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) ;

cluster 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 ) ) minimal positive ) Element of the carrier 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 ) ) -> nilpotent ;

end;

theorem :: BCIALG_2:31

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is ( ( positive ) ( positive ) Element of ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is nilpotent & ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: BCIALG_2:32

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 ( ( 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) iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is nilpotent ) ) ;

theorem :: BCIALG_2:33

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) holds ((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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is minimal ;

theorem :: BCIALG_2:34

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)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is nilpotent holds
ord x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) = ord (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) : ( ( non empty ) ( non empty V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ;

begin

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) ;

mode Congruence of X -> ( ( total symmetric transitive ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) means :: BCIALG_2:def 9
for x, y, u, v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) & [u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) holds
[(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) ;

end;

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) ;

mode L-congruence of X -> ( ( total symmetric transitive ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) means :: BCIALG_2:def 10
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) holds
for u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds [(u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ,(u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) ;

end;

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) ;

mode R-congruence of X -> ( ( total symmetric transitive ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) means :: BCIALG_2:def 11
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) holds
for u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds [(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 ) ) ] : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) ;

end;

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 ( ( ) ( non empty ) Ideal of 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) ) ;

mode I-congruence of X,A -> ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued ) Relation of ) means :: BCIALG_2:def 12
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in it : ( ( ) ( ) Element 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 ) ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier 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 A : ( ( non empty ) ( non empty ) set ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier 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 A : ( ( non empty ) ( non empty ) set ) ) );

end;

registration

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 ( ( ) ( non empty ) Ideal of 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) ) ;

cluster -> total symmetric transitive for ( ( ) ( ) I-congruence 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 ) ,A : ( ( non empty ) ( non empty ) set ) ) ;

end;

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) ;

func IConSet X -> ( ( ) ( ) set ) means :: BCIALG_2:def 13
for A1 being ( ( ) ( ) set ) holds
( A1 : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) iff ex I being ( ( ) ( non empty ) Ideal 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 ) ) st A1 : ( ( ) ( ) set ) is ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) I-congruence 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 ) ,I : ( ( ) ( non empty ) Ideal of 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) ) ) );

end;

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) ;

func ConSet X -> ( ( ) ( ) set ) equals :: BCIALG_2:def 14
{ R : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) R-congruence of 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) ) where R is ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Congruence 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 ) ) : verum } ;

func LConSet X -> ( ( ) ( ) set ) equals :: BCIALG_2:def 15
{ R : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) R-congruence of 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) ) where R is ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) L-congruence 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 ) ) : verum } ;

func RConSet X -> ( ( ) ( ) set ) equals :: BCIALG_2:def 16
{ R : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) R-congruence of 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) ) where R is ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) R-congruence 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 ) ) : verum } ;

end;

theorem :: BCIALG_2:35

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)
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) holds Class (E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) is ( ( closed ) ( non empty closed ) Ideal of 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) ) ;

theorem :: BCIALG_2:36

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)
for R being ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) holds
( R : ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) is ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) iff ( R : ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) is ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) R-congruence of 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) ) & R : ( ( total symmetric transitive ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Equivalence_Relation of ) is ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) L-congruence of 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) ) ) ) ;

theorem :: BCIALG_2:37

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

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 I be ( ( ) ( non empty ) Ideal of 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) ) ;
:: original: I-congruence
redefine mode I-congruence of X,I -> ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Congruence 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 ) ) ;

end;

theorem :: BCIALG_2:38

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 Class (RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) c= I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ;

theorem :: BCIALG_2:39

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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
( I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 closed iff I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) = Class (RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_2:40

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)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( 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 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) in Class (E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( 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 ) ) in Class (E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: BCIALG_2:41

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)
for A, I being ( ( ) ( non empty ) Ideal of 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) )
for IA being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,A : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) )
for II being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 Class (IA : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) = Class (II : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₃ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) holds
IA : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) = II : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₃ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ;

theorem :: BCIALG_2:42

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)
for x, y, u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for k being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) )
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) st [x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) & u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Class (E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) holds
[x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,((y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) to_power k : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) set ) in E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ;

theorem :: BCIALG_2:43

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 ( 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)
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) ex i, j, m, n being ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) st (((x : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(x : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) \ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( ) set ) ) ) to_power i : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) \ x : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 carrier of b₂ : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( ) set ) ) ) to_power j : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = (((y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,(y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) \ x : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 carrier of b₂ : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( ) set ) ) ) to_power m : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,(x : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) \ y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) : ( ( ) ( ) set ) ) ) to_power n : ( ( ) ( V21() V22() V23() V27() V74() ext-real non negative V78() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) holds
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) )
for I being ( ( ) ( non empty ) Ideal of 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) ) st I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) = Class (E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) holds
E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( 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 ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ;

theorem :: BCIALG_2:44

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 IConSet 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) : ( ( ) ( ) set ) c= ConSet 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) : ( ( ) ( ) set ) ;

theorem :: BCIALG_2:45

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 ConSet 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) : ( ( ) ( ) set ) c= LConSet 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) : ( ( ) ( ) set ) ;

theorem :: BCIALG_2:46

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 ConSet 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) : ( ( ) ( ) set ) c= RConSet 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) : ( ( ) ( ) set ) ;

theorem :: BCIALG_2:47

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 ConSet 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) : ( ( ) ( ) set ) = (LConSet 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) ) : ( ( ) ( ) set ) /\ (RConSet 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) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: BCIALG_2:48

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) )
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) st ( for LC being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) L-congruence of 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) ) holds LC : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) L-congruence of b₁ : ( ( 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 ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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
E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) = RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ;

theorem :: BCIALG_2:49

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) )
for E being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of 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) ) st ( for RC being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) R-congruence of 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) ) holds RC : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) R-congruence of b₁ : ( ( 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 ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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
E : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) Congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) = RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ) ;

theorem :: BCIALG_2:50

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)
for LC being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) L-congruence of 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) ) holds Class (LC : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) L-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) ,(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(b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) minimal positive nilpotent ) Element of the carrier of b₁ : ( ( 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) is ( ( closed ) ( non empty closed ) Ideal of 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) ) ;

registration

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

cluster Class E : ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Congruence 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 ) ) : ( ( ) ( ) Element of bool (bool the carrier 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 ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> non empty ;

end;

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

func EqClaOp E -> ( ( Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) ( Relation-like [:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) -defined Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) -valued Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) BinOp of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) means :: BCIALG_2:def 17
for W1, W2 being ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st W1 : ( ( ) ( ) Element of Class E : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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 ) a_partition of the carrier of 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 ) set ) ) ) = Class (E : ( ( non empty ) ( non empty ) set ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier 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 ) : ( ( ) ( non empty ) set ) ) & W2 : ( ( ) ( ) Element of Class E : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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 ) a_partition of the carrier of 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 ) set ) ) ) = Class (E : ( ( non empty ) ( non empty ) set ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier 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 ) : ( ( ) ( non empty ) set ) ) holds
it : ( ( ) ( ) Element 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 ) ) . (W1 : ( ( ) ( ) Element of Class E : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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 ) a_partition of the carrier of 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 ) set ) ) ) ,W2 : ( ( ) ( ) Element of Class E : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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 ) a_partition of the carrier of 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 ) set ) ) ) ) : ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) = Class (E : ( ( non empty ) ( non empty ) set ) ,(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) \ y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier 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 bool the carrier 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 ) : ( ( ) ( non empty ) set ) ) ;

end;

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

func zeroEqC E -> ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) equals :: BCIALG_2:def 18
Class (E : ( ( non empty ) ( 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 ) ) minimal positive nilpotent ) Element of the carrier 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 bool the carrier 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 ) : ( ( ) ( non empty ) set ) ) ;

end;

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

func X ./. E -> ( ( ) ( ) BCIStr_0 ) equals :: BCIALG_2:def 19
BCIStr_0(# (Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(EqClaOp E : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) ( Relation-like [:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) -defined Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) -valued Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) BinOp of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ,(zeroEqC E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) #) : ( ( strict ) ( strict ) BCIStr_0 ) ;

end;

registration

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;

cluster 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 ) ./. E : ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) Congruence 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 ) ) : ( ( ) ( ) BCIStr_0 ) -> non empty ;

end;

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 E be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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) ) ;
let W1, W2 be ( ( ) ( ) Element of Class E : ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) Congruence of 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 ) a_partition of the carrier of 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 ) set ) ) ) ;

func W1 \ W2 -> ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) equals :: BCIALG_2:def 20
(EqClaOp E : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) ( Relation-like [:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) -defined Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) -valued Function-like V18([:(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ,(Class E : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) a_partition of the carrier 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 ) ) :] : ( ( ) ( ) set ) , Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) ) BinOp of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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 ) ) ) . (W1 : ( ( ) ( ) Element 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 ) ) ,W2 : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of Class E : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) a_partition of the carrier 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;

theorem :: BCIALG_2:51

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)
for I being ( ( ) ( non empty ) Ideal of 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) )
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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) ./. RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 ) BCIStr_0 ) is ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ;

registration

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 I be ( ( ) ( non empty ) Ideal of 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) ) ;
let RI be ( ( ) ( Relation-like the carrier of 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 ) set ) -defined the carrier of 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 ) set ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of 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) ) ) ;

cluster 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 ) ./. RI : ( ( ) ( Relation-like the carrier 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 ) -defined the carrier 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 ) -valued total reflexive symmetric transitive ) I-congruence 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 ) ,I : ( ( ) ( non empty ) Ideal 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 ) ) ) : ( ( ) ( ) BCIStr_0 ) -> strict being_B being_C being_I being_BCI-4 ;

end;

theorem :: BCIALG_2:52

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)
for I being ( ( ) ( non empty ) Ideal of 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) ) st I : ( ( ) ( non empty ) Ideal of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ) = BCK-part 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 bool the carrier of b₁ : ( ( 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 ) : ( ( ) ( non empty ) set ) ) holds
for RI being ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of 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) ,I : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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) ./. RI : ( ( ) ( Relation-like the carrier of b₁ : ( ( 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 ) -defined the carrier of b₁ : ( ( 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 ) -valued total reflexive symmetric transitive ) I-congruence of b₁ : ( ( non empty being_B being_C being_I being_BCI-4 ) ( non empty being_B being_C being_I being_BCI-4 ) BCI-algebra) ,b₂ : ( ( ) ( non empty ) Ideal of b₁ : ( ( 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 strict being_B being_C being_I being_BCI-4 ) BCIStr_0 ) is ( ( non empty being_B being_C being_I being_BCI-4 p-Semisimple ) ( non empty being_B being_C being_I being_BCI-4 weakly-positive-implicative p-Semisimple ) BCI-algebra) ;