:: by Tao Sun , Junjie Zhao and Xiquan Liang

::

:: Received November 24, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct BCIStr_1 -> BCIStr_0 , ZeroStr ;

aggr BCIStr_1(# carrier, ExternalDiff, InternalDiff, ZeroF #) -> BCIStr_1 ;

sel ExternalDiff c_{1} -> BinOp of the carrier of c_{1};

end;
struct BCIStr_1 -> BCIStr_0 , ZeroStr ;

aggr BCIStr_1(# carrier, ExternalDiff, InternalDiff, ZeroF #) -> BCIStr_1 ;

sel ExternalDiff c

registration
end;

definition

let A be BCIStr_1 ;

let x, y be Element of A;

coherence

the ExternalDiff of A . (x,y) is Element of A ;

end;
let x, y be Element of A;

coherence

the ExternalDiff of A . (x,y) is Element of A ;

:: deftheorem defines * BCIALG_4:def 1 :

for A being BCIStr_1

for x, y being Element of A holds x * y = the ExternalDiff of A . (x,y);

for A being BCIStr_1

for x, y being Element of A holds x * y = the ExternalDiff of A . (x,y);

definition

let IT be non empty BCIStr_1 ;

end;
attr IT is with_condition_S means :Def2: :: BCIALG_4:def 2

for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z);

for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z);

:: deftheorem Def2 defines with_condition_S BCIALG_4:def 2 :

for IT being non empty BCIStr_1 holds

( IT is with_condition_S iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z) );

for IT being non empty BCIStr_1 holds

( IT is with_condition_S iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y * z) );

Lm1: ( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S )

by STRUCT_0:def 10;

registration

coherence

( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S ) by Lm1;

end;
( BCI_S-EXAMPLE is being_B & BCI_S-EXAMPLE is being_C & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S ) by Lm1;

registration

existence

ex b_{1} being non empty BCIStr_1 st

( b_{1} is strict & b_{1} is being_B & b_{1} is being_C & b_{1} is being_I & b_{1} is being_BCI-4 & b_{1} is with_condition_S )
by Lm1;

end;
ex b

( b

definition

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

end;
definition

let X be BCI-Algebra_with_Condition(S);

let x, y be Element of X;

{ t where t is Element of X : t \ x <= y } is non empty Subset of X

end;
let x, y be Element of X;

func Condition_S (x,y) -> non empty Subset of X equals :: BCIALG_4:def 4

{ t where t is Element of X : t \ x <= y } ;

coherence { t where t is Element of X : t \ x <= y } ;

{ t where t is Element of X : t \ x <= y } is non empty Subset of X

proof end;

:: deftheorem defines Condition_S BCIALG_4:def 4 :

for X being BCI-Algebra_with_Condition(S)

for x, y being Element of X holds Condition_S (x,y) = { t where t is Element of X : t \ x <= y } ;

for X being BCI-Algebra_with_Condition(S)

for x, y being Element of X holds Condition_S (x,y) = { t where t is Element of X : t \ x <= y } ;

theorem :: BCIALG_4:1

for X being BCI-Algebra_with_Condition(S)

for x, y, u, v being Element of X st u in Condition_S (x,y) & v <= u holds

v in Condition_S (x,y)

for x, y, u, v being Element of X st u in Condition_S (x,y) & v <= u holds

v in Condition_S (x,y)

proof end;

theorem :: BCIALG_4:2

for X being BCI-Algebra_with_Condition(S)

for x, y being Element of X ex a being Element of Condition_S (x,y) st

for z being Element of Condition_S (x,y) holds z <= a

for x, y being Element of X ex a being Element of Condition_S (x,y) st

for z being Element of Condition_S (x,y) holds z <= a

proof end;

Lm2: for X being BCI-Algebra_with_Condition(S)

for x, y being Element of X holds

( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds

t <= x * y ) )

proof end;

Lm3: for X being non empty BCIStr_1 st X is BCI-algebra & ( for x, y being Element of X holds

( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds

t <= x * y ) ) ) holds

X is BCI-Algebra_with_Condition(S)

proof end;

theorem :: BCIALG_4:3

definition

let X be p-Semisimple BCI-algebra;

ex b_{1} being strict AbGroup st

( the carrier of b_{1} = the carrier of X & ( for x, y being Element of X holds the addF of b_{1} . (x,y) = x \ ((0. X) \ y) ) & 0. b_{1} = 0. X )

for b_{1}, b_{2} being strict AbGroup st the carrier of b_{1} = the carrier of X & ( for x, y being Element of X holds the addF of b_{1} . (x,y) = x \ ((0. X) \ y) ) & 0. b_{1} = 0. X & the carrier of b_{2} = the carrier of X & ( for x, y being Element of X holds the addF of b_{2} . (x,y) = x \ ((0. X) \ y) ) & 0. b_{2} = 0. X holds

b_{1} = b_{2}

end;
func Adjoint_pGroup X -> strict AbGroup means :: BCIALG_4:def 5

( the carrier of it = the carrier of X & ( for x, y being Element of X holds the addF of it . (x,y) = x \ ((0. X) \ y) ) & 0. it = 0. X );

existence ( the carrier of it = the carrier of X & ( for x, y being Element of X holds the addF of it . (x,y) = x \ ((0. X) \ y) ) & 0. it = 0. X );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines Adjoint_pGroup BCIALG_4:def 5 :

for X being p-Semisimple BCI-algebra

for b_{2} being strict AbGroup holds

( b_{2} = Adjoint_pGroup X iff ( the carrier of b_{2} = the carrier of X & ( for x, y being Element of X holds the addF of b_{2} . (x,y) = x \ ((0. X) \ y) ) & 0. b_{2} = 0. X ) );

for X being p-Semisimple BCI-algebra

for b

( b

::$CT

theorem Th4: :: BCIALG_4:5

for X being BCI-algebra holds

( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds

x = y )

( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds

x = y )

proof end;

theorem :: BCIALG_4:6

for X being BCI-Algebra_with_Condition(S) st X is p-Semisimple holds

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

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

proof end;

theorem Th7: :: BCIALG_4:8

for X being BCI-Algebra_with_Condition(S)

for x, y, z being Element of X st x <= y holds

( x * z <= y * z & z * x <= z * y )

for x, y, z being Element of X st x <= y holds

( x * z <= y * z & z * x <= z * y )

proof end;

theorem Th8: :: BCIALG_4:9

for X being BCI-Algebra_with_Condition(S)

for x being Element of X holds

( (0. X) * x = x & x * (0. X) = x )

for x being Element of X holds

( (0. X) * x = x & x * (0. X) = x )

proof end;

theorem Th9: :: BCIALG_4:10

for X being BCI-Algebra_with_Condition(S)

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

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

proof end;

theorem Th10: :: BCIALG_4:11

for X being BCI-Algebra_with_Condition(S)

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

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

proof end;

theorem Th11: :: BCIALG_4:12

for X being BCI-Algebra_with_Condition(S)

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

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

proof end;

theorem :: BCIALG_4:14

for X being BCI-Algebra_with_Condition(S)

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

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

proof end;

theorem :: BCIALG_4:15

theorem :: BCIALG_4:16

for X being BCI-Algebra_with_Condition(S)

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

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

proof end;

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

proof end;

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

proof end;

registration

let X be BCI-Algebra_with_Condition(S);

coherence

( the ExternalDiff of X is commutative & the ExternalDiff of X is associative ) by Lm4, Lm5;

end;
coherence

( the ExternalDiff of X is commutative & the ExternalDiff of X is associative ) by Lm4, Lm5;

definition

let X be BCI-Algebra_with_Condition(S);

ex b_{1} being Function of [: the carrier of X,NAT:], the carrier of X st

for h being Element of X holds

( b_{1} . (h,0) = 0. X & ( for n being Nat holds b_{1} . (h,(n + 1)) = (b_{1} . (h,n)) * h ) )

for b_{1}, b_{2} being Function of [: the carrier of X,NAT:], the carrier of X st ( for h being Element of X holds

( b_{1} . (h,0) = 0. X & ( for n being Nat holds b_{1} . (h,(n + 1)) = (b_{1} . (h,n)) * h ) ) ) & ( for h being Element of X holds

( b_{2} . (h,0) = 0. X & ( for n being Nat holds b_{2} . (h,(n + 1)) = (b_{2} . (h,n)) * h ) ) ) holds

b_{1} = b_{2}

end;
func power X -> Function of [: the carrier of X,NAT:], the carrier of X means :Def6: :: BCIALG_4:def 6

for h being Element of X holds

( it . (h,0) = 0. X & ( for n being Nat holds it . (h,(n + 1)) = (it . (h,n)) * h ) );

existence for h being Element of X holds

( it . (h,0) = 0. X & ( for n being Nat holds it . (h,(n + 1)) = (it . (h,n)) * h ) );

ex b

for h being Element of X holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def6 defines power BCIALG_4:def 6 :

for X being BCI-Algebra_with_Condition(S)

for b_{2} being Function of [: the carrier of X,NAT:], the carrier of X holds

( b_{2} = power X iff for h being Element of X holds

( b_{2} . (h,0) = 0. X & ( for n being Nat holds b_{2} . (h,(n + 1)) = (b_{2} . (h,n)) * h ) ) );

for X being BCI-Algebra_with_Condition(S)

for b

( b

( b

definition

let X be BCI-Algebra_with_Condition(S);

let x be Element of X;

let n be Nat;

correctness

coherence

(power X) . (x,n) is Element of X;

;

end;
let x be Element of X;

let n be Nat;

correctness

coherence

(power X) . (x,n) is Element of X;

;

:: deftheorem defines |^ BCIALG_4:def 7 :

for X being BCI-Algebra_with_Condition(S)

for x being Element of X

for n being Nat holds x |^ n = (power X) . (x,n);

for X being BCI-Algebra_with_Condition(S)

for x being Element of X

for n being Nat holds x |^ n = (power X) . (x,n);

theorem :: BCIALG_4:20

theorem :: BCIALG_4:21

Lm6: for n being Nat

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

proof end;

theorem :: BCIALG_4:27

for X being BCI-Algebra_with_Condition(S)

for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3)

for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3)

proof end;

Lm7: for X being BCI-Algebra_with_Condition(S)

for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0)

proof end;

theorem :: BCIALG_4:28

for n being Nat

for X being BCI-Algebra_with_Condition(S)

for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)

for X being BCI-Algebra_with_Condition(S)

for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)

proof end;

definition

let X be non empty BCIStr_1 ;

let F be FinSequence of the carrier of X;

correctness

coherence

the ExternalDiff of X "**" F is Element of X;

;

end;
let F be FinSequence of the carrier of X;

correctness

coherence

the ExternalDiff of X "**" F is Element of X;

;

:: deftheorem defines Product_S BCIALG_4:def 8 :

for X being non empty BCIStr_1

for F being FinSequence of the carrier of X holds Product_S F = the ExternalDiff of X "**" F;

for X being non empty BCIStr_1

for F being FinSequence of the carrier of X holds Product_S F = the ExternalDiff of X "**" F;

theorem :: BCIALG_4:30

for X being BCI-Algebra_with_Condition(S)

for F1, F2 being FinSequence of the carrier of X holds Product_S (F1 ^ F2) = (Product_S F1) * (Product_S F2) by Th18, FINSOP_1:5;

for F1, F2 being FinSequence of the carrier of X holds Product_S (F1 ^ F2) = (Product_S F1) * (Product_S F2) by Th18, FINSOP_1:5;

theorem :: BCIALG_4:31

for X being BCI-Algebra_with_Condition(S)

for F being FinSequence of the carrier of X

for a being Element of X holds Product_S (F ^ <*a*>) = (Product_S F) * a by Th18, FINSOP_1:4;

for F being FinSequence of the carrier of X

for a being Element of X holds Product_S (F ^ <*a*>) = (Product_S F) * a by Th18, FINSOP_1:4;

theorem :: BCIALG_4:32

for X being BCI-Algebra_with_Condition(S)

for F being FinSequence of the carrier of X

for a being Element of X holds Product_S (<*a*> ^ F) = a * (Product_S F) by Th18, FINSOP_1:6;

for F being FinSequence of the carrier of X

for a being Element of X holds Product_S (<*a*> ^ F) = a * (Product_S F) by Th18, FINSOP_1:6;

theorem Th32: :: BCIALG_4:33

for X being BCI-Algebra_with_Condition(S)

for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2

for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2

proof end;

theorem Th33: :: BCIALG_4:34

for X being BCI-Algebra_with_Condition(S)

for a1, a2, a3 being Element of X holds Product_S <*a1,a2,a3*> = (a1 * a2) * a3

for a1, a2, a3 being Element of X holds Product_S <*a1,a2,a3*> = (a1 * a2) * a3

proof end;

theorem :: BCIALG_4:35

for X being BCI-Algebra_with_Condition(S)

for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)

for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>)

proof end;

theorem :: BCIALG_4:36

for X being BCI-Algebra_with_Condition(S)

for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)

for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>)

proof end;

theorem :: BCIALG_4:37

for X being BCI-Algebra_with_Condition(S)

for a, b being Element of AtomSet X

for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds

ex mb being Element of X st

for y being Element of BranchV b holds y <= mb

for a, b being Element of AtomSet X

for ma being Element of X st ( for x being Element of BranchV a holds x <= ma ) holds

ex mb being Element of X st

for y being Element of BranchV b holds y <= mb

proof end;

:: Commutative BCK-Algebras with Condition(S)

registration

ex b_{1} being BCI-Algebra_with_Condition(S) st

( b_{1} is strict & b_{1} is being_BCK-5 )
by Lm1;

end;

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

existence ex b

( b

theorem Th37: :: BCIALG_4:38

for X being BCK-Algebra_with_Condition(S)

for x, y being Element of X holds

( x <= x * y & y <= x * y )

for x, y being Element of X holds

( x <= x * y & y <= x * y )

proof end;

theorem :: BCIALG_4:39

for X being BCK-Algebra_with_Condition(S)

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

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

proof end;

theorem :: BCIALG_4:40

for X being BCK-Algebra_with_Condition(S)

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

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

proof end;

theorem :: BCIALG_4:41

for X being BCK-Algebra_with_Condition(S)

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

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

proof end;

definition

let IT be BCK-Algebra_with_Condition(S);

end;
attr IT is commutative means :Def9: :: BCIALG_4:def 9

for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);

for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);

:: deftheorem Def9 defines commutative BCIALG_4:def 9 :

for IT being BCK-Algebra_with_Condition(S) holds

( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

for IT being BCK-Algebra_with_Condition(S) holds

( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );

registration

ex b_{1} being BCK-Algebra_with_Condition(S) st b_{1} is commutative
end;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative for BCIStr_1 ;

existence ex b

proof end;

theorem :: BCIALG_4:42

for X being non empty BCIStr_1 holds

( X is commutative BCK-Algebra_with_Condition(S) iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) )

( X is commutative BCK-Algebra_with_Condition(S) iff for x, y, z being Element of X holds

( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) )

proof end;

theorem :: BCIALG_4:43

for X being commutative BCK-Algebra_with_Condition(S)

for a being Element of X st a is greatest holds

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

for a being Element of X st a is greatest holds

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

proof end;

definition

let X be BCI-algebra;

let a be Element of X;

{ t where t is Element of X : t <= a } is non empty Subset of X

end;
let a be Element of X;

func Initial_section a -> non empty Subset of X equals :: BCIALG_4:def 10

{ t where t is Element of X : t <= a } ;

coherence { t where t is Element of X : t <= a } ;

{ t where t is Element of X : t <= a } is non empty Subset of X

proof end;

:: deftheorem defines Initial_section BCIALG_4:def 10 :

for X being BCI-algebra

for a being Element of X holds Initial_section a = { t where t is Element of X : t <= a } ;

for X being BCI-algebra

for a being Element of X holds Initial_section a = { t where t is Element of X : t <= a } ;

theorem :: BCIALG_4:44

for X being commutative BCK-Algebra_with_Condition(S)

for a, b, c being Element of X st Condition_S (a,b) c= Initial_section c holds

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

for a, b, c being Element of X st Condition_S (a,b) c= Initial_section c holds

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

proof end;

:: Positive-Implicative BCK-Algebras with Condition(S)

definition

let IT be BCK-Algebra_with_Condition(S);

end;
attr IT is positive-implicative means :: BCIALG_4:def 11

for x, y being Element of IT holds (x \ y) \ y = x \ y;

for x, y being Element of IT holds (x \ y) \ y = x \ y;

:: deftheorem defines positive-implicative BCIALG_4:def 11 :

for IT being BCK-Algebra_with_Condition(S) holds

( IT is positive-implicative iff for x, y being Element of IT holds (x \ y) \ y = x \ y );

for IT being BCK-Algebra_with_Condition(S) holds

( IT is positive-implicative iff for x, y being Element of IT holds (x \ y) \ y = x \ y );

registration

ex b_{1} being BCK-Algebra_with_Condition(S) st b_{1} is positive-implicative
end;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S positive-implicative for BCIStr_1 ;

existence ex b

proof end;

theorem Th44: :: BCIALG_4:45

for X being BCK-Algebra_with_Condition(S) holds

( X is positive-implicative iff for x being Element of X holds x * x = x )

( X is positive-implicative iff for x being Element of X holds x * x = x )

proof end;

theorem Th45: :: BCIALG_4:46

for X being BCK-Algebra_with_Condition(S) holds

( X is positive-implicative iff for x, y being Element of X st x <= y holds

x * y = y )

( X is positive-implicative iff for x, y being Element of X st x <= y holds

x * y = y )

proof end;

theorem Th46: :: BCIALG_4:47

for X being BCK-Algebra_with_Condition(S) holds

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

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

proof end;

theorem Th47: :: BCIALG_4:48

for X being BCK-Algebra_with_Condition(S) holds

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

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

proof end;

theorem Th48: :: BCIALG_4:49

for X being positive-implicative BCK-Algebra_with_Condition(S)

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

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

proof end;

definition

let IT be non empty BCIStr_1 ;

end;
attr IT is being_SB-2 means :Def13: :: BCIALG_4:def 13

for x, y being Element of IT holds x * y = y * x;

for x, y being Element of IT holds x * y = y * x;

attr IT is being_SB-4 means :Def14: :: BCIALG_4:def 14

for x, y being Element of IT holds (x \ y) * y = x * y;

for x, y being Element of IT holds (x \ y) * y = x * y;

:: deftheorem Def12 defines being_SB-1 BCIALG_4:def 12 :

for IT being non empty BCIStr_1 holds

( IT is being_SB-1 iff for x being Element of IT holds x * x = x );

for IT being non empty BCIStr_1 holds

( IT is being_SB-1 iff for x being Element of IT holds x * x = x );

:: deftheorem Def13 defines being_SB-2 BCIALG_4:def 13 :

for IT being non empty BCIStr_1 holds

( IT is being_SB-2 iff for x, y being Element of IT holds x * y = y * x );

for IT being non empty BCIStr_1 holds

( IT is being_SB-2 iff for x, y being Element of IT holds x * y = y * x );

:: deftheorem Def14 defines being_SB-4 BCIALG_4:def 14 :

for IT being non empty BCIStr_1 holds

( IT is being_SB-4 iff for x, y being Element of IT holds (x \ y) * y = x * y );

for IT being non empty BCIStr_1 holds

( IT is being_SB-4 iff for x, y being Element of IT holds (x \ y) * y = x * y );

Lm8: ( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S )

by STRUCT_0:def 10;

registration

coherence

( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S ) by Lm8;

end;
( BCI_S-EXAMPLE is being_SB-1 & BCI_S-EXAMPLE is being_SB-2 & BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S ) by Lm8;

registration

existence

ex b_{1} being non empty BCIStr_1 st

( b_{1} is strict & b_{1} is being_SB-1 & b_{1} is being_SB-2 & b_{1} is being_SB-4 & b_{1} is being_I & b_{1} is with_condition_S )
by Lm8;

end;
ex b

( b

definition

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

end;
theorem :: BCIALG_4:50

for X being non empty BCIStr_1 holds

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

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

proof end;

:: Implicative BCK-Algebras with Condition(S)

:: deftheorem defines implicative BCIALG_4:def 15 :

for IT being BCK-Algebra_with_Condition(S) holds

( IT is implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

for IT being BCK-Algebra_with_Condition(S) holds

( IT is implicative iff for x, y being Element of IT holds x \ (y \ x) = x );

registration

ex b_{1} being BCK-Algebra_with_Condition(S) st b_{1} is implicative
end;

cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S implicative for BCIStr_1 ;

existence ex b

proof end;

theorem Th50: :: BCIALG_4:51

for X being BCK-Algebra_with_Condition(S) holds

( X is implicative iff ( X is commutative & X is positive-implicative ) )

( X is implicative iff ( X is commutative & X is positive-implicative ) )

proof end;

theorem :: BCIALG_4:52

for X being BCK-Algebra_with_Condition(S) holds

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

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

proof end;