:: BCI-Algebras with Condition (S) and Their Properties
:: by Tao Sun , Junjie Zhao and Xiquan Liang
::
:: Received November 24, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct BCIStr_1  ->  BCIStr_0 , ZeroStr ;
aggrBCIStr_1(# carrier, ExternalDiff, InternalDiff, ZeroF #) ->  BCIStr_1 ;
sel ExternalDiff c1 ->  BinOp of the carrier of c1;
end;

registration
cluster non empty strict for BCIStr_1 ;
existence
 ex b1 being BCIStr_1 st
( not b1 is empty & b1 is strict )
proofend;
end;

definition
let A be BCIStr_1 ;
let x, y be Element of A;
funcx * y ->  Element of A equals :: BCIALG_4:def 1
 the ExternalDiff of A . (x,y);
coherence
 the ExternalDiff of A . (x,y) is Element of A ;
end;

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

definition
let IT be non empty BCIStr_1 ;
attrIT 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);
end;

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

definition
func BCI_S-EXAMPLE  ->  BCIStr_1  equals :: BCIALG_4:def 3
 BCIStr_1(# 1,op2,op2,op0 #);
coherence
 BCIStr_1(# 1,op2,op2,op0 #) is BCIStr_1 ;
end;

:: deftheorem  defines BCI_S-EXAMPLE BCIALG_4:def_3_:_
 BCI_S-EXAMPLE = BCIStr_1(# 1,op2,op2,op0 #);

registration
cluster BCI_S-EXAMPLE  -> 1 -element strict ;
coherence
 ( BCI_S-EXAMPLE is strict & BCI_S-EXAMPLE is 1 -element ) by STRUCT_0:def_19, CARD_1:49;
end;

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

registration
cluster BCI_S-EXAMPLE  ->  being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S ;
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;

registration
cluster non empty being_B being_C being_I being_BCI-4 strict with_condition_S for BCIStr_1 ;
existence
 ex b1 being non empty BCIStr_1 st
( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is with_condition_S ) by Lm1;
end;

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;
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  }  is non empty Subset of X
proofend;
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  }  ;

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) &amp; v <= u holds
v in Condition_S (x,y)
proofend;

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

Lm2:  for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds
( (x * y) \ x <= y &amp; ( for t being Element of X st t \ x <= y holds
t <= x * y ) )
proofend;

Lm3:  for X being non empty BCIStr_1 st X is BCI-algebra &amp; ( for x, y being Element of X holds
( (x * y) \ x <= y &amp; ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) holds
X is BCI-Algebra_with_Condition(S)
proofend;

theorem :: BCIALG_4:3
for X being non empty BCIStr_1 holds
( ( X is BCI-algebra &amp; ( for x, y being Element of X holds
( (x * y) \ x <= y &amp; ( for t being Element of X st t \ x <= y holds
t <= x * y ) ) ) ) iff X is BCI-Algebra_with_Condition(S) ) by Lm2, Lm3;

theorem :: BCIALG_4:4
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
proofend;

definition
let X be p-Semisimple BCI-algebra;
func Adjoint_pGroup X ->  strict AbGroup means :: BCIALG_4:def 5
( the carrier of it = the carrier of X &amp; ( for x, y being Element of X holds the addF of it . (x,y) = x \ ((0. X) \ y) ) &amp; 0. it = 0. X );
existence
 ex b1 being strict AbGroup st
( the carrier of b1 = the carrier of X &amp; ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) &amp; 0. b1 = 0. X )
proofend;
uniqueness
 for b1, b2 being strict AbGroup st the carrier of b1 = the carrier of X &amp; ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) &amp; 0. b1 = 0. X &amp; the carrier of b2 = the carrier of X &amp; ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) &amp; 0. b2 = 0. X holds
b1 = b2
proofend;
end;

:: deftheorem  defines Adjoint_pGroup BCIALG_4:def_5_:_
 for X being p-Semisimple BCI-algebra
for b2 being strict AbGroup holds
( b2 = Adjoint_pGroup X iff ( the carrier of b2 = the carrier of X &amp; ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) &amp; 0. b2 = 0. X ) );

theorem Th5: :: 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 )
proofend;

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

theorem Th7: :: BCIALG_4:7
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds x * y = y * x
proofend;

theorem Th8: :: 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 &amp; z * x <= z * y )
proofend;

theorem Th9: :: BCIALG_4:9
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds
( (0. X) * x = x &amp; x * (0. X) = x )
proofend;

theorem Th10: :: 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)
proofend;

theorem Th11: :: 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
proofend;

theorem Th12: :: 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)
proofend;

theorem Th13: :: BCIALG_4:13
for X being BCI-Algebra_with_Condition(S)
for x, y being Element of X holds y <= x * (y \ x)
proofend;

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

theorem :: BCIALG_4:15
for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds
( x \ y <= z iff x <= y * z )
proofend;

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

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

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

registration
let X be BCI-Algebra_with_Condition(S);
cluster the ExternalDiff of X ->  commutative associative ;
coherence
 ( the ExternalDiff of X is commutative &amp; the ExternalDiff of X is associative ) by Lm4, Lm5;
end;

theorem Th17: :: BCIALG_4:17
for X being BCI-Algebra_with_Condition(S) holds 0. X is_a_unity_wrt the ExternalDiff of X
proofend;

theorem :: BCIALG_4:18
for X being BCI-Algebra_with_Condition(S) holds the_unity_wrt the ExternalDiff of X = 0. X
proofend;

theorem Th19: :: BCIALG_4:19
for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is having_a_unity
proofend;

definition
let X be BCI-Algebra_with_Condition(S);
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 &amp; ( for n being Element of NAT holds it . (h,(n + 1)) = (it . (h,n)) * h ) );
existence
 ex b1 being Function of [: the carrier of X,NAT:], the carrier of X st
for h being Element of X holds
( b1 . (h,0) = 0. X &amp; ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) )
proofend;
uniqueness
 for b1, b2 being Function of [: the carrier of X,NAT:], the carrier of X st ( for h being Element of X holds
( b1 . (h,0) = 0. X &amp; ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) &amp; ( for h being Element of X holds
( b2 . (h,0) = 0. X &amp; ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines power BCIALG_4:def_6_:_
 for X being BCI-Algebra_with_Condition(S)
for b2 being Function of [: the carrier of X,NAT:], the carrier of X holds
( b2 = power X iff for h being Element of X holds
( b2 . (h,0) = 0. X &amp; ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) );

definition
let X be BCI-Algebra_with_Condition(S);
let x be Element of X;
let n be Element of NAT ;
funcx |^ n ->  Element of X equals :: BCIALG_4:def 7
(power X) . (x,n);
correctness
coherence
(power X) . (x,n) is Element of X;
;
end;

:: deftheorem  defines |^ BCIALG_4:def_7_:_
 for X being BCI-Algebra_with_Condition(S)
for x being Element of X
for n being Element of NAT holds x |^ n = (power X) . (x,n);

theorem :: BCIALG_4:20
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 0 = 0. X by Def6;

theorem :: BCIALG_4:21
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ (n + 1) = (x |^ n) * x by Def6;

theorem Th22: :: BCIALG_4:22
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 1 = x
proofend;

theorem Th23: :: BCIALG_4:23
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 2 = x * x
proofend;

theorem :: BCIALG_4:24
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ 3 = (x * x) * x
proofend;

theorem Th25: :: BCIALG_4:25
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ 2 = 0. X
proofend;

Lm6:  for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X
proofend;

theorem :: BCIALG_4:26
for n being Element of NAT
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X
proofend;

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

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

theorem :: BCIALG_4:28
for n being Element of 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)
proofend;

definition
let X be non empty BCIStr_1 ;
let F be FinSequence of the carrier of X;
func Product_S F ->  Element of X equals :: BCIALG_4:def 8
 the ExternalDiff of X "**" F;
correctness
coherence
the ExternalDiff of X "**" F is Element of X;
;
end;

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

theorem :: BCIALG_4:29
for X being non empty BCIStr_1
for d being Element of X holds the ExternalDiff of X "**" <*d*> = d
proofend;

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 Th19, 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 Th19, 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 Th19, FINSOP_1:6;

theorem Th33: :: 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
proofend;

theorem Th34: :: 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
proofend;

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

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

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

:: Commutative BCK-Algebras with Condition(S)
registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 strict with_condition_S for BCIStr_1 ;
existence
 ex b1 being BCI-Algebra_with_Condition(S) st
( b1 is strict &amp; b1 is being_BCK-5 ) by Lm1;
end;

definition
mode BCK-Algebra_with_Condition(S) is being_BCK-5 BCI-Algebra_with_Condition(S);
end;

theorem Th38: :: BCIALG_4:38
for X being BCK-Algebra_with_Condition(S)
for x, y being Element of X holds
( x <= x * y &amp; y <= x * y )
proofend;

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

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

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

definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is commutative  means :Def9: :: BCIALG_4:def 9
 for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x);
end;

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

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S commutative for BCIStr_1 ;
existence
 ex b1 being BCK-Algebra_with_Condition(S) st b1 is commutative
proofend;
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 &amp; (x \ z) \ (x \ y) = (y \ z) \ (y \ x) &amp; (x \ y) \ z = x \ (y * z) ) )
proofend;

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

definition
let X be BCI-algebra;
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  }  is non empty Subset of X
proofend;
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  }  ;

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

:: Positive-Implicative BCK-Algebras with Condition(S)
definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is positive-implicative  means :Def11: :: BCIALG_4:def 11
 for x, y being Element of IT holds (x \ y) \ y = x \ y;
end;

:: deftheorem Def11 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 );

registration
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 b1 being BCK-Algebra_with_Condition(S) st b1 is positive-implicative
proofend;
end;

theorem Th45: :: 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 )
proofend;

theorem Th46: :: 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 )
proofend;

theorem Th47: :: 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) )
proofend;

theorem Th48: :: 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) )
proofend;

theorem Th49: :: 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))
proofend;

definition
let IT be non empty BCIStr_1 ;
attrIT is being_SB-1  means :Def12: :: BCIALG_4:def 12
 for x being Element of IT holds x * x = x;
attrIT is being_SB-2  means :Def13: :: BCIALG_4:def 13
 for x, y being Element of IT holds x * y = y * x;
attrIT is being_SB-4  means :Def14: :: BCIALG_4:def 14
 for x, y being Element of IT holds (x \ y) * y = x * y;
end;

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

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

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

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

registration
cluster BCI_S-EXAMPLE  ->  being_I with_condition_S being_SB-1 being_SB-2 being_SB-4 ;
coherence
 ( BCI_S-EXAMPLE is being_SB-1 &amp; BCI_S-EXAMPLE is being_SB-2 &amp; BCI_S-EXAMPLE is being_SB-4 &amp; BCI_S-EXAMPLE is being_I &amp; BCI_S-EXAMPLE is with_condition_S ) by Lm8;
end;

registration
cluster non empty being_I strict with_condition_S being_SB-1 being_SB-2 being_SB-4 for BCIStr_1 ;
existence
 ex b1 being non empty BCIStr_1 st
( b1 is strict &amp; b1 is being_SB-1 &amp; b1 is being_SB-2 &amp; b1 is being_SB-4 &amp; b1 is being_I &amp; b1 is with_condition_S ) by Lm8;
end;

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

:: Implicative BCK-Algebras with Condition(S)
definition
let IT be BCK-Algebra_with_Condition(S);
attrIT is implicative  means :Def15: :: BCIALG_4:def 15
 for x, y being Element of IT holds x \ (y \ x) = x;
end;

:: deftheorem Def15 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 );

registration
cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 with_condition_S implicative for BCIStr_1 ;
existence
 ex b1 being BCK-Algebra_with_Condition(S) st b1 is implicative
proofend;
end;

theorem Th51: :: BCIALG_4:51
for X being BCK-Algebra_with_Condition(S) holds
( X is implicative iff ( X is commutative &amp; X is positive-implicative ) )
proofend;

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