:: BCIALG_4 semantic presentation 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 ) proof set A = the non empty set ; set m = the BinOp of the non empty set ; set u = the Element of the non empty set ; take BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: ( not BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty & BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict ) thus not the carrier of BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict thus BCIStr_1(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict ; ::_thesis: verum end; 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 ) proof thus BCI_S-EXAMPLE is being_B ::_thesis: ( 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 ) proof let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_3 ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI_S-EXAMPLE thus ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_C ::_thesis: ( 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 ) proof let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_4 ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI_S-EXAMPLE thus ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_I ::_thesis: ( BCI_S-EXAMPLE is being_BCI-4 & BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S ) proof let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. BCI_S-EXAMPLE thus x \ x = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_BCI-4 ::_thesis: ( BCI_S-EXAMPLE is being_BCK-5 & BCI_S-EXAMPLE is with_condition_S ) proof let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_7 ::_thesis: ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y ) thus ( not x \ y = 0. BCI_S-EXAMPLE or not y \ x = 0. BCI_S-EXAMPLE or x = y ) by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_BCK-5 ::_thesis: BCI_S-EXAMPLE is with_condition_S proof let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_1:def_8 ::_thesis: x ` = 0. BCI_S-EXAMPLE thus x ` = 0. BCI_S-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_2 ::_thesis: (x \ y) \ z = x \ (y * z) thus (x \ y) \ z = x \ (y * z) by STRUCT_0:def_10; ::_thesis: verum end; 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 proof set a = (0. X) \ (((0. X) \ x) \ y); set Y = { t where t is Element of X : t \ x <= y } ; A1: now__::_thesis:_for_y1_being_set_st_y1_in__{__t_where_t_is_Element_of_X_:_t_\_x_<=_y__}__holds_ y1_in_the_carrier_of_X let y1 be set ; ::_thesis: ( y1 in { t where t is Element of X : t \ x <= y } implies y1 in the carrier of X ) assume y1 in { t where t is Element of X : t \ x <= y } ; ::_thesis: y1 in the carrier of X then ex x1 being Element of X st ( y1 = x1 & x1 \ x <= y ) ; hence y1 in the carrier of X ; ::_thesis: verum end; (((0. X) \ (((0. X) \ x) \ y)) \ x) \ y = (((0. X) \ x) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:7 .= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ y by BCIALG_1:2 .= ((((0. X) \ x) \ (0. X)) \ (((0. X) \ x) \ y)) \ (y \ (0. X)) by BCIALG_1:2 .= 0. X by BCIALG_1:1 ; then ((0. X) \ (((0. X) \ x) \ y)) \ x <= y by BCIALG_1:def_11; then (0. X) \ (((0. X) \ x) \ y) in { t where t is Element of X : t \ x <= y } ; hence { t where t is Element of X : t \ x <= y } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum end; 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) & v <= u holds v in Condition_S (x,y) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: 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) let x, y, u, v be Element of X; ::_thesis: ( u in Condition_S (x,y) & v <= u implies v in Condition_S (x,y) ) assume that A1: u in Condition_S (x,y) and A2: v <= u ; ::_thesis: v in Condition_S (x,y) v \ x <= u \ x by A2, BCIALG_1:5; then A3: (v \ x) \ (u \ x) = 0. X by BCIALG_1:def_11; ex u1 being Element of X st ( u = u1 & u1 \ x <= y ) by A1; then (u \ x) \ y = 0. X by BCIALG_1:def_11; then (v \ x) \ y = 0. X by A3, BCIALG_1:3; then v \ x <= y by BCIALG_1:def_11; hence v in Condition_S (x,y) ; ::_thesis: verum 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: 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 let x, y be Element of X; ::_thesis: ex a being Element of Condition_S (x,y) st for z being Element of Condition_S (x,y) holds z <= a ((x * y) \ x) \ y = (x * y) \ (x * y) by Def2 .= 0. X by BCIALG_1:def_5 ; then (x * y) \ x <= y by BCIALG_1:def_11; then x * y in { t where t is Element of X : t \ x <= y } ; then consider u being Element of Condition_S (x,y) such that A1: u = x * y ; take u ; ::_thesis: for z being Element of Condition_S (x,y) holds z <= u for z being Element of Condition_S (x,y) holds z <= u proof let z be Element of Condition_S (x,y); ::_thesis: z <= u z in { t where t is Element of X : t \ x <= y } ; then consider z1 being Element of X such that A2: z = z1 and A3: z1 \ x <= y ; z \ u = (z1 \ x) \ y by A1, A2, Def2 .= 0. X by A3, BCIALG_1:def_11 ; hence z <= u by BCIALG_1:def_11; ::_thesis: verum end; hence for z being Element of Condition_S (x,y) holds z <= u ; ::_thesis: verum 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 let X be BCI-Algebra_with_Condition(S); ::_thesis: 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 ) ) let x, y be Element of X; ::_thesis: ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds t <= x * y ) ) A1: for t being Element of X st t \ x <= y holds t <= x * y proof let t be Element of X; ::_thesis: ( t \ x <= y implies t <= x * y ) assume A2: t \ x <= y ; ::_thesis: t <= x * y t \ (x * y) = (t \ x) \ y by Def2 .= 0. X by A2, BCIALG_1:def_11 ; hence t <= x * y by BCIALG_1:def_11; ::_thesis: verum end; ((x * y) \ x) \ y = (x * y) \ (x * y) by Def2 .= 0. X by BCIALG_1:def_5 ; hence ( (x * y) \ x <= y & ( for t being Element of X st t \ x <= y holds t <= x * y ) ) by A1, BCIALG_1:def_11; ::_thesis: verum 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 let X be non empty BCIStr_1 ; ::_thesis: ( 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 ) ) ) implies X is BCI-Algebra_with_Condition(S) ) assume that A1: X is BCI-algebra and A2: 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 ) ) ; ::_thesis: X is BCI-Algebra_with_Condition(S) for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = x \ (y * z) (y * z) \ y <= z by A2; then A3: ((y * z) \ y) \ z = 0. X by BCIALG_1:def_11; (x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by A1, BCIALG_1:7 .= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by A1, BCIALG_1:2 ; then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by A1, BCIALG_1:11; then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) by BCIALG_1:def_11; then (x \ ((x \ y) \ z)) \ y <= z by A1, BCIALG_1:2; then x \ ((x \ y) \ z) <= y * z by A2; then (x \ ((x \ y) \ z)) \ (y * z) = 0. X by BCIALG_1:def_11; then A4: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by A1, BCIALG_1:7; ((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X by A1, BCIALG_1:11; then ((x \ y) \ (x \ (y * z))) \ z = 0. X by A1, A3, BCIALG_1:3; then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by A1, BCIALG_1:7; hence (x \ y) \ z = x \ (y * z) by A1, A4, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCI-Algebra_with_Condition(S) by A1, Def2; ::_thesis: verum end; theorem :: BCIALG_4:3 for X being non empty BCIStr_1 holds ( ( 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 ) ) ) ) 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: 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 let x, y be Element of X; ::_thesis: ex a being Element of Condition_S (x,y) st for z being Element of Condition_S (x,y) holds z <= a ex a being Element of Condition_S (x,y) st for z being Element of Condition_S (x,y) holds z <= a proof (x * y) \ x <= y by Lm2; then x * y in Condition_S (x,y) ; then consider a being Element of Condition_S (x,y) such that A1: a = x * y ; take a ; ::_thesis: for z being Element of Condition_S (x,y) holds z <= a for t1 being Element of Condition_S (x,y) holds t1 <= a proof let t1 be Element of Condition_S (x,y); ::_thesis: t1 <= a t1 in { t where t is Element of X : t \ x <= y } ; then ex t2 being Element of X st ( t2 = t1 & t2 \ x <= y ) ; hence t1 <= a by A1, Lm2; ::_thesis: verum end; hence for z being Element of Condition_S (x,y) holds z <= a ; ::_thesis: verum end; hence ex a being Element of Condition_S (x,y) st for z being Element of Condition_S (x,y) holds z <= a ; ::_thesis: verum end; 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 & ( for x, y being Element of X holds the addF of it . (x,y) = x \ ((0. X) \ y) ) & 0. it = 0. X ); existence ex b1 being strict AbGroup st ( the carrier of b1 = the carrier of X & ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) & 0. b1 = 0. X ) proof reconsider A0 = 0. X as Element of X ; defpred S1[ Element of X, Element of X, Element of X] means ex x, y being Element of X st ( $1 = x & $2 = y & $3 = x \ ((0. X) \ y) ); A1: for a, b being Element of X ex c being Element of X st S1[a,b,c] proof let a, b be Element of X; ::_thesis: ex c being Element of X st S1[a,b,c] reconsider x = a, y = b as Element of X ; reconsider c = x \ ((0. X) \ y) as Element of X ; take c ; ::_thesis: S1[a,b,c] thus S1[a,b,c] ; ::_thesis: verum end; consider h being BinOp of the carrier of X such that A2: for a, b being Element of X holds S1[a,b,h . (a,b)] from BINOP_1:sch_3(A1); set G = addLoopStr(# the carrier of X,h,A0 #); A3: for x, y being Element of X holds h . (x,y) = x \ ((0. X) \ y) proof let x, y be Element of X; ::_thesis: h . (x,y) = x \ ((0. X) \ y) ex x9, y9 being Element of X st ( x = x9 & y = y9 & h . (x,y) = x9 \ ((0. X) \ y9) ) by A2; hence h . (x,y) = x \ ((0. X) \ y) ; ::_thesis: verum end; A4: for a being Element of X ex b, x being Element of X st ( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) proof let a be Element of X; ::_thesis: ex b, x being Element of X st ( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) reconsider x = a as Element of X ; reconsider b = (0. X) \ x as Element of X ; A5: b \ ((0. X) \ x) = 0. X by BCIALG_1:def_5; take b ; ::_thesis: ex x being Element of X st ( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) x \ ((0. X) \ b) = x \ ((x `) `) .= x \ x by BCIALG_1:54 .= 0. X by BCIALG_1:def_5 ; hence ex x being Element of X st ( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A5; ::_thesis: verum end; ( addLoopStr(# the carrier of X,h,A0 #) is Abelian & addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable ) proof thus addLoopStr(# the carrier of X,h,A0 #) is Abelian ::_thesis: ( addLoopStr(# the carrier of X,h,A0 #) is add-associative & addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable ) proof let a, b be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a reconsider x = a, y = b as Element of X ; thus a + b = x \ ((0. X) \ y) by A3 .= y \ ((0. X) \ x) by BCIALG_1:57 .= b + a by A3 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_3 ::_thesis: ( addLoopStr(# the carrier of X,h,A0 #) is right_zeroed & addLoopStr(# the carrier of X,h,A0 #) is right_complementable ) let a, b, c be Element of addLoopStr(# the carrier of X,h,A0 #); ::_thesis: (a + b) + c = a + (b + c) reconsider x = a, y = b, z = c as Element of X ; thus (a + b) + c = h . ((x \ ((0. X) \ y)),z) by A3 .= (x \ ((0. X) \ y)) \ ((0. X) \ z) by A3 .= (y \ ((0. X) \ x)) \ ((0. X) \ z) by BCIALG_1:57 .= (y \ ((0. X) \ z)) \ ((0. X) \ x) by BCIALG_1:7 .= x \ ((0. X) \ (y \ ((0. X) \ z))) by BCIALG_1:57 .= h . (x,(y \ ((0. X) \ z))) by A3 .= a + (b + c) by A3 ; ::_thesis: verum end; hereby :: according to RLVECT_1:def_4 ::_thesis: addLoopStr(# the carrier of X,h,A0 #) is right_complementable let a be Element of addLoopStr(# the carrier of X,h,A0 #); ::_thesis: a + (0. addLoopStr(# the carrier of X,h,A0 #)) = a reconsider x = a as Element of X ; thus a + (0. addLoopStr(# the carrier of X,h,A0 #)) = x \ ((0. X) \ (0. X)) by A3 .= x \ (0. X) by BCIALG_1:2 .= a by BCIALG_1:2 ; ::_thesis: verum end; let a be Element of addLoopStr(# the carrier of X,h,A0 #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable consider b being Element of X such that A6: ex x being Element of X st ( a = x & x \ ((0. X) \ b) = 0. X & b \ ((0. X) \ x) = 0. X ) by A4; reconsider b = b as Element of addLoopStr(# the carrier of X,h,A0 #) ; take b ; :: according to ALGSTR_0:def_11 ::_thesis: a + b = 0. addLoopStr(# the carrier of X,h,A0 #) thus a + b = 0. addLoopStr(# the carrier of X,h,A0 #) by A3, A6; ::_thesis: verum end; then reconsider G = addLoopStr(# the carrier of X,h,A0 #) as strict AbGroup ; take G ; ::_thesis: ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X ) thus ( the carrier of G = the carrier of X & ( for x, y being Element of X holds the addF of G . (x,y) = x \ ((0. X) \ y) ) & 0. G = 0. X ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being strict AbGroup st the carrier of b1 = the carrier of X & ( for x, y being Element of X holds the addF of b1 . (x,y) = x \ ((0. X) \ y) ) & 0. b1 = 0. X & the carrier of b2 = the carrier of X & ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) & 0. b2 = 0. X holds b1 = b2 proof thus for G1, G2 being strict AbGroup st the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X holds G1 = G2 ::_thesis: verum proof let G1, G2 be strict AbGroup; ::_thesis: ( the carrier of G1 = the carrier of X & ( for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) ) & 0. G1 = 0. X & the carrier of G2 = the carrier of X & ( for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) ) & 0. G2 = 0. X implies G1 = G2 ) assume that A7: the carrier of G1 = the carrier of X and A8: for x, y being Element of X holds the addF of G1 . (x,y) = x \ ((0. X) \ y) and A9: ( 0. G1 = 0. X & the carrier of G2 = the carrier of X ) and A10: for x, y being Element of X holds the addF of G2 . (x,y) = x \ ((0. X) \ y) and A11: 0. G2 = 0. X ; ::_thesis: G1 = G2 now__::_thesis:_for_a,_b_being_Element_of_G1_holds_the_addF_of_G1_._(a,b)_=_the_addF_of_G2_._(a,b) let a, b be Element of G1; ::_thesis: the addF of G1 . (a,b) = the addF of G2 . (a,b) reconsider x = a, y = b as Element of X by A7; thus the addF of G1 . (a,b) = x \ ((0. X) \ y) by A8 .= the addF of G2 . (a,b) by A10 ; ::_thesis: verum end; hence G1 = G2 by A7, A9, A11, BINOP_1:2; ::_thesis: verum end; end; 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 & ( for x, y being Element of X holds the addF of b2 . (x,y) = x \ ((0. X) \ y) ) & 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 ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X st x \ y = 0. X holds x = y ) thus ( X is p-Semisimple implies for x, y being Element of X st x \ y = 0. X holds x = y ) ::_thesis: ( ( for x, y being Element of X st x \ y = 0. X holds x = y ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x, y being Element of X st x \ y = 0. X holds x = y for x, y being Element of X st x \ y = 0. X holds x = y proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y ) assume A2: x \ y = 0. X ; ::_thesis: x = y (0. X) \ (x \ y) = (y \ x) \ ((0. X) `) by A1, BCIALG_1:66 .= (y \ x) \ (0. X) by BCIALG_1:def_5 .= y \ x by BCIALG_1:2 ; then y \ x = 0. X by A2, BCIALG_1:def_5; hence x = y by A2, BCIALG_1:def_7; ::_thesis: verum end; hence for x, y being Element of X st x \ y = 0. X holds x = y ; ::_thesis: verum end; assume A3: for x, y being Element of X st x \ y = 0. X holds x = y ; ::_thesis: X is p-Semisimple for x, y being Element of X holds x \ (x \ y) = y proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence x \ (x \ y) = y by A3; ::_thesis: verum end; hence X is p-Semisimple by BCIALG_1:def_26; ::_thesis: verum 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: ( X is p-Semisimple implies for x, y being Element of X holds x * y = x \ ((0. X) \ y) ) assume A1: X is p-Semisimple ; ::_thesis: 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 let x, y be Element of X; ::_thesis: x * y = x \ ((0. X) \ y) set z1 = x \ ((0. X) \ y); set z2 = x * y; ((x \ ((0. X) \ y)) \ x) \ y = ((x \ x) \ ((0. X) \ y)) \ y by BCIALG_1:7 .= ((0. X) \ ((0. X) \ y)) \ y by BCIALG_1:def_5 .= ((0. X) \ y) \ ((0. X) \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then (x \ ((0. X) \ y)) \ x <= y by BCIALG_1:def_11; then x \ ((0. X) \ y) <= x * y by Lm2; then A2: (x \ ((0. X) \ y)) \ (x * y) = 0. X by BCIALG_1:def_11; A3: for t being Element of X st t \ x <= y holds t <= x \ ((0. X) \ y) proof let t be Element of X; ::_thesis: ( t \ x <= y implies t <= x \ ((0. X) \ y) ) assume t \ x <= y ; ::_thesis: t <= x \ ((0. X) \ y) then (t \ x) \ y = 0. X by BCIALG_1:def_11; then t \ (x \ ((0. X) \ y)) = t \ (x \ ((0. X) \ (t \ x))) by A1, Th5 .= t \ (x \ (x \ (t \ (0. X)))) by A1, BCIALG_1:57 .= t \ (t \ (0. X)) by A1, BCIALG_1:61 .= t \ t by BCIALG_1:2 .= 0. X by BCIALG_1:def_5 ; hence t <= x \ ((0. X) \ y) by BCIALG_1:def_11; ::_thesis: verum end; (x * y) \ x <= y by Lm2; then x * y <= x \ ((0. X) \ y) by A3; then (x * y) \ (x \ ((0. X) \ y)) = 0. X by BCIALG_1:def_11; hence x * y = x \ ((0. X) \ y) by A2, BCIALG_1:def_7; ::_thesis: verum end; hence for x, y being Element of X holds x * y = x \ ((0. X) \ y) ; ::_thesis: verum end; 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds x * y = y * x let x, y be Element of X; ::_thesis: x * y = y * x (y * x) \ y <= x by Lm2; then ((y * x) \ y) \ x = 0. X by BCIALG_1:def_11; then ((y * x) \ x) \ y = 0. X by BCIALG_1:7; then (y * x) \ x <= y by BCIALG_1:def_11; then y * x <= x * y by Lm2; then A1: (y * x) \ (x * y) = 0. X by BCIALG_1:def_11; (x * y) \ x <= y by Lm2; then ((x * y) \ x) \ y = 0. X by BCIALG_1:def_11; then ((x * y) \ y) \ x = 0. X by BCIALG_1:7; then (x * y) \ y <= x by BCIALG_1:def_11; then x * y <= y * x by Lm2; then (x * y) \ (y * x) = 0. X by BCIALG_1:def_11; hence x * y = y * x by A1, BCIALG_1:def_7; ::_thesis: verum end; 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 & z * x <= z * y ) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X st x <= y holds ( x * z <= y * z & z * x <= z * y ) let x, y, z be Element of X; ::_thesis: ( x <= y implies ( x * z <= y * z & z * x <= z * y ) ) assume x <= y ; ::_thesis: ( x * z <= y * z & z * x <= z * y ) then (x * z) \ y <= (x * z) \ x by BCIALG_1:5; then A1: ((x * z) \ y) \ ((x * z) \ x) = 0. X by BCIALG_1:def_11; (x * z) \ x <= z by Lm2; then ((x * z) \ x) \ z = 0. X by BCIALG_1:def_11; then ((x * z) \ y) \ z = 0. X by A1, BCIALG_1:3; then A2: (x * z) \ y <= z by BCIALG_1:def_11; ( x * z = z * x & y * z = z * y ) by Th7; hence ( x * z <= y * z & z * x <= z * y ) by A2, Lm2; ::_thesis: verum end; theorem Th9: :: 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 ) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds ( (0. X) * x = x & x * (0. X) = x ) let x be Element of X; ::_thesis: ( (0. X) * x = x & x * (0. X) = x ) (x \ (0. X)) \ x = (x \ x) \ (0. X) by BCIALG_1:7 .= (0. X) \ (0. X) by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_5 ; then x \ (0. X) <= x by BCIALG_1:def_11; then x <= (0. X) * x by Lm2; then A1: x \ ((0. X) * x) = 0. X by BCIALG_1:def_11; ((0. X) * x) \ (0. X) <= x by Lm2; then (0. X) * x <= x by BCIALG_1:2; then ((0. X) * x) \ x = 0. X by BCIALG_1:def_11; then (0. X) * x = x by A1, BCIALG_1:def_7; hence ( (0. X) * x = x & x * (0. X) = x ) by Th7; ::_thesis: verum end; 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * y) * z = x * (y * z) let x, y, z be Element of X; ::_thesis: (x * y) * z = x * (y * z) A1: (z * (x * y)) \ z <= x * y by Lm2; (((x * y) * z) \ x) \ z = (((x * y) * z) \ z) \ x by BCIALG_1:7 .= ((z * (x * y)) \ z) \ x by Th7 ; then (((x * y) * z) \ x) \ z <= (x * y) \ x by A1, BCIALG_1:5; then A2: ((((x * y) * z) \ x) \ z) \ ((x * y) \ x) = 0. X by BCIALG_1:def_11; A3: (x * (z * y)) \ x <= z * y by Lm2; (((z * y) * x) \ z) \ x = (((z * y) * x) \ x) \ z by BCIALG_1:7 .= ((x * (z * y)) \ x) \ z by Th7 ; then (((z * y) * x) \ z) \ x <= (z * y) \ z by A3, BCIALG_1:5; then A4: ((((z * y) * x) \ z) \ x) \ ((z * y) \ z) = 0. X by BCIALG_1:def_11; (z * y) \ z <= y by Lm2; then ((z * y) \ z) \ y = 0. X by BCIALG_1:def_11; then ((((z * y) * x) \ z) \ x) \ y = 0. X by A4, BCIALG_1:3; then (((z * y) * x) \ z) \ x <= y by BCIALG_1:def_11; then ((z * y) * x) \ z <= x * y by Lm2; then (z * y) * x <= z * (x * y) by Lm2; then (y * z) * x <= z * (x * y) by Th7; then x * (y * z) <= z * (x * y) by Th7; then x * (y * z) <= (x * y) * z by Th7; then A5: (x * (y * z)) \ ((x * y) * z) = 0. X by BCIALG_1:def_11; (x * y) \ x <= y by Lm2; then ((x * y) \ x) \ y = 0. X by BCIALG_1:def_11; then ((((x * y) * z) \ x) \ z) \ y = 0. X by A2, BCIALG_1:3; then (((x * y) * z) \ x) \ z <= y by BCIALG_1:def_11; then ((x * y) * z) \ x <= z * y by Lm2; then (x * y) * z <= x * (z * y) by Lm2; then (x * y) * z <= x * (y * z) by Th7; then ((x * y) * z) \ (x * (y * z)) = 0. X by BCIALG_1:def_11; hence (x * y) * z = x * (y * z) by A5, BCIALG_1:def_7; ::_thesis: verum end; 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * y) * z = (x * z) * y let x, y, z be Element of X; ::_thesis: (x * y) * z = (x * z) * y (x * y) * z = x * (y * z) by Th10 .= (y * z) * x by Th7 .= y * (z * x) by Th10 .= (z * x) * y by Th7 ; hence (x * y) * z = (x * z) * y by Th7; ::_thesis: verum end; 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x \ y) \ z = x \ (y * z) let x, y, z be Element of X; ::_thesis: (x \ y) \ z = x \ (y * z) (x \ ((x \ y) \ z)) \ y = (x \ y) \ ((x \ y) \ z) by BCIALG_1:7 .= ((x \ y) \ (0. X)) \ ((x \ y) \ z) by BCIALG_1:2 ; then ((x \ ((x \ y) \ z)) \ y) \ (z \ (0. X)) = 0. X by BCIALG_1:11; then (x \ ((x \ y) \ z)) \ y <= z \ (0. X) by BCIALG_1:def_11; then (x \ ((x \ y) \ z)) \ y <= z by BCIALG_1:2; then x \ ((x \ y) \ z) <= y * z by Lm2; then (x \ ((x \ y) \ z)) \ (y * z) = 0. X by BCIALG_1:def_11; then A1: (x \ (y * z)) \ ((x \ y) \ z) = 0. X by BCIALG_1:7; (y * z) \ y <= z by Lm2; then ( ((x \ y) \ (x \ (y * z))) \ ((y * z) \ y) = 0. X & ((y * z) \ y) \ z = 0. X ) by BCIALG_1:11, BCIALG_1:def_11; then ((x \ y) \ (x \ (y * z))) \ z = 0. X by BCIALG_1:3; then ((x \ y) \ z) \ (x \ (y * z)) = 0. X by BCIALG_1:7; hence (x \ y) \ z = x \ (y * z) by A1, BCIALG_1:def_7; ::_thesis: verum end; 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y being Element of X holds y <= x * (y \ x) let x, y be Element of X; ::_thesis: y <= x * (y \ x) (y \ x) \ (y \ x) = 0. X by BCIALG_1:def_5; then y \ x <= y \ x by BCIALG_1:def_11; hence y <= x * (y \ x) by Lm2; ::_thesis: verum 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds (x * z) \ (y * z) <= x \ y let x, y, z be Element of X; ::_thesis: (x * z) \ (y * z) <= x \ y x <= y * (x \ y) by Th13; then x * z <= (y * (x \ y)) * z by Th8; then x * z <= (y * z) * (x \ y) by Th11; then (x * z) \ (y * z) <= ((y * z) * (x \ y)) \ (y * z) by BCIALG_1:5; then A1: ((x * z) \ (y * z)) \ (((y * z) * (x \ y)) \ (y * z)) = 0. X by BCIALG_1:def_11; ((y * z) * (x \ y)) \ (y * z) <= x \ y by Lm2; then (((y * z) * (x \ y)) \ (y * z)) \ (x \ y) = 0. X by BCIALG_1:def_11; then ((x * z) \ (y * z)) \ (x \ y) = 0. X by A1, BCIALG_1:3; hence (x * z) \ (y * z) <= x \ y by BCIALG_1:def_11; ::_thesis: verum end; 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 ) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds ( x \ y <= z iff x <= y * z ) A1: for x, y, z being Element of X st x <= y * z holds x \ y <= z proof let x, y, z be Element of X; ::_thesis: ( x <= y * z implies x \ y <= z ) assume x <= y * z ; ::_thesis: x \ y <= z then x \ (y * z) = 0. X by BCIALG_1:def_11; then (x \ y) \ z = 0. X by Th12; hence x \ y <= z by BCIALG_1:def_11; ::_thesis: verum end; for x, y, z being Element of X st x \ y <= z holds x <= y * z proof let x, y, z be Element of X; ::_thesis: ( x \ y <= z implies x <= y * z ) assume x \ y <= z ; ::_thesis: x <= y * z then (x \ y) \ z = 0. X by BCIALG_1:def_11; then x \ (y * z) = 0. X by Th12; hence x <= y * z by BCIALG_1:def_11; ::_thesis: verum end; hence for x, y, z being Element of X holds ( x \ y <= z iff x <= y * z ) by A1; ::_thesis: verum end; 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, y, z being Element of X holds x \ y <= (x \ z) * (z \ y) let x, y, z be Element of X; ::_thesis: x \ y <= (x \ z) * (z \ y) ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by BCIALG_1:11; then (x \ y) \ ((x \ z) * (z \ y)) = 0. X by Th12; hence x \ y <= (x \ z) * (z \ y) by BCIALG_1:def_11; ::_thesis: verum end; Lm4: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is commutative proof let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is commutative now__::_thesis:_for_a,_b_being_Element_of_X_holds_the_ExternalDiff_of_X_._(a,b)_=_the_ExternalDiff_of_X_._(b,a) let a, b be Element of X; ::_thesis: the ExternalDiff of X . (a,b) = the ExternalDiff of X . (b,a) thus the ExternalDiff of X . (a,b) = a * b .= b * a by Th7 .= the ExternalDiff of X . (b,a) ; ::_thesis: verum end; hence the ExternalDiff of X is commutative by BINOP_1:def_2; ::_thesis: verum end; Lm5: for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is associative proof let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is associative now__::_thesis:_for_a,_b,_c_being_Element_of_X_holds_the_ExternalDiff_of_X_._(a,(_the_ExternalDiff_of_X_._(b,c)))_=_the_ExternalDiff_of_X_._((_the_ExternalDiff_of_X_._(a,b)),c) let a, b, c be Element of X; ::_thesis: the ExternalDiff of X . (a,( the ExternalDiff of X . (b,c))) = the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c) thus the ExternalDiff of X . (a,( the ExternalDiff of X . (b,c))) = a * (b * c) .= (a * b) * c by Th10 .= the ExternalDiff of X . (( the ExternalDiff of X . (a,b)),c) ; ::_thesis: verum end; hence the ExternalDiff of X is associative by BINOP_1:def_3; ::_thesis: verum end; registration let X be BCI-Algebra_with_Condition(S); cluster the ExternalDiff of X -> commutative associative ; coherence ( the ExternalDiff of X is commutative & 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: 0. X is_a_unity_wrt the ExternalDiff of X now__::_thesis:_for_a_being_Element_of_X_holds_ (_the_ExternalDiff_of_X_._((0._X),a)_=_a_&_the_ExternalDiff_of_X_._(a,(0._X))_=_a_) let a be Element of X; ::_thesis: ( the ExternalDiff of X . ((0. X),a) = a & the ExternalDiff of X . (a,(0. X)) = a ) thus the ExternalDiff of X . ((0. X),a) = (0. X) * a .= a by Th9 ; ::_thesis: the ExternalDiff of X . (a,(0. X)) = a thus the ExternalDiff of X . (a,(0. X)) = a * (0. X) .= a by Th9 ; ::_thesis: verum end; hence 0. X is_a_unity_wrt the ExternalDiff of X by BINOP_1:3; ::_thesis: verum end; theorem :: BCIALG_4:18 for X being BCI-Algebra_with_Condition(S) holds the_unity_wrt the ExternalDiff of X = 0. X proof let X be BCI-Algebra_with_Condition(S); ::_thesis: the_unity_wrt the ExternalDiff of X = 0. X reconsider e = 0. X as Element of X ; e is_a_unity_wrt the ExternalDiff of X by Th17; hence the_unity_wrt the ExternalDiff of X = 0. X by BINOP_1:def_8; ::_thesis: verum end; theorem Th19: :: BCIALG_4:19 for X being BCI-Algebra_with_Condition(S) holds the ExternalDiff of X is having_a_unity proof let X be BCI-Algebra_with_Condition(S); ::_thesis: the ExternalDiff of X is having_a_unity reconsider e = 0. X as Element of X ; e is_a_unity_wrt the ExternalDiff of X by Th17; hence the ExternalDiff of X is having_a_unity by SETWISEO:def_2; ::_thesis: verum end; 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 & ( 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 & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) proof defpred S1[ set , set ] means ex g0 being Function of NAT, the carrier of X ex h being Element of X st ( $1 = h & g0 = $2 & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h ) ); A1: for x being set st x in the carrier of X holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier of X implies ex y being set st S1[x,y] ) assume x in the carrier of X ; ::_thesis: ex y being set st S1[x,y] then reconsider b = x as Element of X ; deffunc H1( Nat, Element of X) -> Element of X = $2 * b; consider g0 being Function of NAT, the carrier of X such that A2: g0 . 0 = 0. X and A3: for n being Nat holds g0 . (n + 1) = H1(n,g0 . n) from NAT_1:sch_12(); reconsider y = g0 as set ; take y ; ::_thesis: S1[x,y] take g0 ; ::_thesis: ex h being Element of X st ( x = h & g0 = y & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h ) ) take b ; ::_thesis: ( x = b & g0 = y & g0 . 0 = 0. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * b ) ) thus ( x = b & g0 = y & g0 . 0 = 0. X ) by A2; ::_thesis: for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * b let n be Element of NAT ; ::_thesis: g0 . (n + 1) = (g0 . n) * b thus g0 . (n + 1) = (g0 . n) * b by A3; ::_thesis: verum end; consider f being Function such that dom f = the carrier of X and A4: for x being set st x in the carrier of X holds S1[x,f . x] from CLASSES1:sch_1(A1); defpred S2[ Element of X, Element of NAT , set ] means ex g0 being Function of NAT, the carrier of X st ( g0 = f . $1 & $3 = g0 . $2 ); A5: for a being Element of X for n being Element of NAT ex b being Element of X st S2[a,n,b] proof let a be Element of X; ::_thesis: for n being Element of NAT ex b being Element of X st S2[a,n,b] let n be Element of NAT ; ::_thesis: ex b being Element of X st S2[a,n,b] consider g0 being Function of NAT, the carrier of X, h being Element of X such that a = h and A6: g0 = f . a and g0 . 0 = 0. X and for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * h by A4; take g0 . n ; ::_thesis: S2[a,n,g0 . n] take g0 ; ::_thesis: ( g0 = f . a & g0 . n = g0 . n ) thus ( g0 = f . a & g0 . n = g0 . n ) by A6; ::_thesis: verum end; consider F being Function of [: the carrier of X,NAT:], the carrier of X such that A7: for a being Element of X for n being Element of NAT holds S2[a,n,F . (a,n)] from BINOP_1:sch_3(A5); take F ; ::_thesis: for h being Element of X holds ( F . (h,0) = 0. X & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) ) let h be Element of X; ::_thesis: ( F . (h,0) = 0. X & ( for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h ) ) A8: ex g2 being Function of NAT, the carrier of X ex b being Element of X st ( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Element of NAT holds g2 . (n + 1) = (g2 . n) * b ) ) by A4; ex g1 being Function of NAT, the carrier of X st ( g1 = f . h & F . (h,0) = g1 . 0 ) by A7; hence F . (h,0) = 0. X by A8; ::_thesis: for n being Element of NAT holds F . (h,(n + 1)) = (F . (h,n)) * h let n be Element of NAT ; ::_thesis: F . (h,(n + 1)) = (F . (h,n)) * h A9: ex g2 being Function of NAT, the carrier of X ex b being Element of X st ( h = b & g2 = f . h & g2 . 0 = 0. X & ( for n being Element of NAT holds g2 . (n + 1) = (g2 . n) * b ) ) by A4; ( ex g0 being Function of NAT, the carrier of X st ( g0 = f . h & F . (h,n) = g0 . n ) & ex g1 being Function of NAT, the carrier of X st ( g1 = f . h & F . (h,(n + 1)) = g1 . (n + 1) ) ) by A7; hence F . (h,(n + 1)) = (F . (h,n)) * h by A9; ::_thesis: verum end; 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 & ( for n being Element of NAT holds b1 . (h,(n + 1)) = (b1 . (h,n)) * h ) ) ) & ( for h being Element of X holds ( b2 . (h,0) = 0. X & ( for n being Element of NAT holds b2 . (h,(n + 1)) = (b2 . (h,n)) * h ) ) ) holds b1 = b2 proof let f, g be Function of [: the carrier of X,NAT:], the carrier of X; ::_thesis: ( ( for h being Element of X holds ( f . (h,0) = 0. X & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) ) & ( for h being Element of X holds ( g . (h,0) = 0. X & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ) implies f = g ) assume that A10: for h being Element of X holds ( f . (h,0) = 0. X & ( for n being Element of NAT holds f . (h,(n + 1)) = (f . (h,n)) * h ) ) and A11: for h being Element of X holds ( g . (h,0) = 0. X & ( for n being Element of NAT holds g . (h,(n + 1)) = (g . (h,n)) * h ) ) ; ::_thesis: f = g now__::_thesis:_for_h_being_Element_of_X for_n_being_Element_of_NAT_holds_f_._(h,n)_=_g_._(h,n) let h be Element of X; ::_thesis: for n being Element of NAT holds f . (h,n) = g . (h,n) let n be Element of NAT ; ::_thesis: f . (h,n) = g . (h,n) defpred S1[ Element of NAT ] means f . [h,$1] = g . [h,$1]; A12: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A13: S1[n] ; ::_thesis: S1[n + 1] A14: g . [h,n] = g . (h,n) ; f . [h,(n + 1)] = f . (h,(n + 1)) .= (f . (h,n)) * h by A10 .= g . (h,(n + 1)) by A11, A13, A14 .= g . [h,(n + 1)] ; hence S1[n + 1] ; ::_thesis: verum end; f . [h,0] = f . (h,0) .= 0. X by A10 .= g . (h,0) by A11 .= g . [h,0] ; then A15: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A15, A12); hence f . (h,n) = g . (h,n) ; ::_thesis: verum end; hence f = g by BINOP_1:2; ::_thesis: verum end; 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 & ( 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 1 = x let x be Element of X; ::_thesis: x |^ 1 = x thus x |^ 1 = x |^ (0 + 1) .= (x |^ 0) * x by Def6 .= (0. X) * x by Def6 .= x by Th9 ; ::_thesis: verum end; theorem Th23: :: BCIALG_4:23 for X being BCI-Algebra_with_Condition(S) for x being Element of X holds x |^ 2 = x * x proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 2 = x * x let x be Element of X; ::_thesis: x |^ 2 = x * x thus x |^ 2 = x |^ (1 + 1) .= (x |^ 1) * x by Def6 .= x * x by Th22 ; ::_thesis: verum end; theorem :: BCIALG_4:24 for X being BCI-Algebra_with_Condition(S) for x being Element of X holds x |^ 3 = (x * x) * x proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x being Element of X holds x |^ 3 = (x * x) * x let x be Element of X; ::_thesis: x |^ 3 = (x * x) * x thus x |^ 3 = x |^ (2 + 1) .= (x |^ 2) * x by Def6 .= (x * x) * x by Th23 ; ::_thesis: verum end; theorem Th25: :: BCIALG_4:25 for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ 2 = 0. X proof let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ 2 = 0. X (0. X) * (0. X) = ((0. X) * (0. X)) \ (0. X) by BCIALG_1:2; then (0. X) * (0. X) <= 0. X by Lm2; then A1: ((0. X) * (0. X)) \ (0. X) = 0. X by BCIALG_1:def_11; 0. X <= (0. X) * ((0. X) \ (0. X)) by Th13; then 0. X <= (0. X) * (0. X) by BCIALG_1:def_5; then (0. X) \ ((0. X) * (0. X)) = 0. X by BCIALG_1:def_11; then (0. X) * (0. X) = 0. X by A1, BCIALG_1:def_7; hence (0. X) |^ 2 = 0. X by Th23; ::_thesis: verum end; Lm6: for n being Element of NAT for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X proof let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ (n + 1) = 0. X let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ (n + 1) = 0. X defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds (0. X) |^ (m + 1) = 0. X; now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_ (0._X)_|^_(m_+_1)_=_0._X_)_holds_ for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_ (0._X)_|^_(m_+_1)_=_0._X let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds (0. X) |^ (m + 1) = 0. X ) implies for m being Element of NAT st m = k + 1 & m <= n holds (0. X) |^ (m + 1) = 0. X ) assume A1: for m being Element of NAT st m = k & m <= n holds (0. X) |^ (m + 1) = 0. X ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds (0. X) |^ (m + 1) = 0. X let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (0. X) |^ (m + 1) = 0. X ) assume that A2: m = k + 1 and A3: m <= n ; ::_thesis: (0. X) |^ (m + 1) = 0. X k <= n by A2, A3, NAT_1:13; then A4: (0. X) |^ (k + 1) = 0. X by A1; A5: (0. X) |^ 2 = 0. X by Th25; (0. X) |^ (m + 1) = ((0. X) |^ (k + 1)) * (0. X) by A2, Def6; hence (0. X) |^ (m + 1) = 0. X by A5, A4, Th23; ::_thesis: verum end; then A6: for k being Element of NAT st S1[k] holds S1[k + 1] ; A7: S1[ 0 ] by Th22; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); hence (0. X) |^ (n + 1) = 0. X ; ::_thesis: verum end; theorem :: BCIALG_4:26 for n being Element of NAT for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X proof let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X let X be BCI-Algebra_with_Condition(S); ::_thesis: (0. X) |^ n = 0. X defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds (0. X) |^ m = 0. X; A1: for k being Element of NAT st S1[k] holds S1[k + 1] by Lm6; A2: S1[ 0 ] by Def6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); hence (0. X) |^ n = 0. X ; ::_thesis: verum 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) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds ((x \ a) \ a) \ a = x \ (a |^ 3) let x, a be Element of X; ::_thesis: ((x \ a) \ a) \ a = x \ (a |^ 3) (x \ a) \ a = x \ (a * a) by Th12; then ((x \ a) \ a) \ a = x \ ((a * a) * a) by Th12 .= x \ ((a |^ 2) * a) by Th23 .= x \ (a |^ (2 + 1)) by Def6 ; hence ((x \ a) \ a) \ a = x \ (a |^ 3) ; ::_thesis: verum 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 let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds (x,a) to_power 0 = x \ (a |^ 0) let x, a be Element of X; ::_thesis: (x,a) to_power 0 = x \ (a |^ 0) x \ (a |^ 0) = x \ (0. X) by Def6 .= x by BCIALG_1:2 ; hence (x,a) to_power 0 = x \ (a |^ 0) by BCIALG_2:1; ::_thesis: verum end; 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) proof let n be Element of NAT ; ::_thesis: for X being BCI-Algebra_with_Condition(S) for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n) let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n) let x, a be Element of X; ::_thesis: (x,a) to_power n = x \ (a |^ n) defpred S1[ set ] means for m being Element of NAT st m = $1 & m <= n holds (x,a) to_power m = x \ (a |^ m); now__::_thesis:_for_k_being_Element_of_NAT_st_(_for_m_being_Element_of_NAT_st_m_=_k_&_m_<=_n_holds_ (x,a)_to_power_m_=_x_\_(a_|^_m)_)_holds_ for_m_being_Element_of_NAT_st_m_=_k_+_1_&_m_<=_n_holds_ (x,a)_to_power_m_=_x_\_(a_|^_m) let k be Element of NAT ; ::_thesis: ( ( for m being Element of NAT st m = k & m <= n holds (x,a) to_power m = x \ (a |^ m) ) implies for m being Element of NAT st m = k + 1 & m <= n holds (x,a) to_power m = x \ (a |^ m) ) assume A1: for m being Element of NAT st m = k & m <= n holds (x,a) to_power m = x \ (a |^ m) ; ::_thesis: for m being Element of NAT st m = k + 1 & m <= n holds (x,a) to_power m = x \ (a |^ m) let m be Element of NAT ; ::_thesis: ( m = k + 1 & m <= n implies (x,a) to_power m = x \ (a |^ m) ) assume that A2: m = k + 1 and A3: m <= n ; ::_thesis: (x,a) to_power m = x \ (a |^ m) A4: ( (x,a) to_power m = ((x,a) to_power k) \ a & k <= n ) by A2, A3, BCIALG_2:4, NAT_1:13; x \ (a |^ m) = x \ ((a |^ k) * a) by A2, Def6 .= (x \ (a |^ k)) \ a by Th12 ; hence (x,a) to_power m = x \ (a |^ m) by A1, A4; ::_thesis: verum end; then A5: for k being Element of NAT st S1[k] holds S1[k + 1] ; A6: S1[ 0 ] by Lm7; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5); hence (x,a) to_power n = x \ (a |^ n) ; ::_thesis: verum end; 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 proof let X be non empty BCIStr_1 ; ::_thesis: for d being Element of X holds the ExternalDiff of X "**" <*d*> = d let d be Element of X; ::_thesis: the ExternalDiff of X "**" <*d*> = d A1: len <*d*> = 1 by FINSEQ_1:39; then ex f being Function of NAT, the carrier of X st ( f . 1 = <*d*> . 1 & ( for n being Element of NAT st 0 <> n & n < len <*d*> holds f . (n + 1) = the ExternalDiff of X . ((f . n),(<*d*> . (n + 1))) ) & the ExternalDiff of X "**" <*d*> = f . (len <*d*>) ) by FINSOP_1:def_1; hence the ExternalDiff of X "**" <*d*> = d by A1, FINSEQ_1:def_8; ::_thesis: verum end; 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for a1, a2 being Element of X holds Product_S <*a1,a2*> = a1 * a2 let a1, a2 be Element of X; ::_thesis: Product_S <*a1,a2*> = a1 * a2 thus Product_S <*a1,a2*> = (Product_S <*a1*>) * a2 by Th19, FINSOP_1:4 .= a1 * a2 by FINSOP_1:11 ; ::_thesis: verum end; 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for a1, a2, a3 being Element of X holds Product_S <*a1,a2,a3*> = (a1 * a2) * a3 let a1, a2, a3 be Element of X; ::_thesis: Product_S <*a1,a2,a3*> = (a1 * a2) * a3 thus Product_S <*a1,a2,a3*> = (Product_S <*a1,a2*>) * a3 by Th19, FINSOP_1:4 .= (a1 * a2) * a3 by FINSOP_1:12 ; ::_thesis: verum 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*>) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a1, a2 being Element of X holds (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) let x, a1, a2 be Element of X; ::_thesis: (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) (x \ a1) \ a2 = x \ (a1 * a2) by Th12; hence (x \ a1) \ a2 = x \ (Product_S <*a1,a2*>) by Th33; ::_thesis: verum 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*>) proof let X be BCI-Algebra_with_Condition(S); ::_thesis: for x, a1, a2, a3 being Element of X holds ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>) let x, a1, a2, a3 be Element of X; ::_thesis: ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>) ((x \ a1) \ a2) \ a3 = (x \ (a1 * a2)) \ a3 by Th12 .= x \ ((a1 * a2) * a3) by Th12 ; hence ((x \ a1) \ a2) \ a3 = x \ (Product_S <*a1,a2,a3*>) by Th34; ::_thesis: verum 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 proof let X be BCI-Algebra_with_Condition(S); ::_thesis: 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 let a, b be Element of AtomSet X; ::_thesis: 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 let ma be Element of X; ::_thesis: ( ( for x being Element of BranchV a holds x <= ma ) implies ex mb being Element of X st for y being Element of BranchV b holds y <= mb ) assume A1: for x being Element of BranchV a holds x <= ma ; ::_thesis: ex mb being Element of X st for y being Element of BranchV b holds y <= mb ex mb being Element of X st for y being Element of BranchV b holds y <= mb proof set mb = (b * ((0. X) \ a)) * ma; for y being Element of BranchV b holds y <= (b * ((0. X) \ a)) * ma proof a \ a = 0. X by BCIALG_1:def_5; then a <= a by BCIALG_1:def_11; then a in { yy2 where yy2 is Element of X : a <= yy2 } ; then A2: a is Element of BranchV a ; let y be Element of BranchV b; ::_thesis: y <= (b * ((0. X) \ a)) * ma 0. X in AtomSet X ; then consider x0 being Element of AtomSet X such that A3: x0 = 0. X ; y in { yy where yy is Element of X : b <= yy } ; then ex yy being Element of X st ( y = yy & b <= yy ) ; then b \ b <= y \ b by BCIALG_1:5; then y \ b in { yy1 where yy1 is Element of X : b \ b <= yy1 } ; then A4: y \ b is Element of BranchV (b \ b) ; A5: (b \ b) \ (x0 \ a) = x0 \ (x0 \ a) by A3, BCIALG_1:def_5 .= a by BCIALG_1:24 ; x0 \ x0 = 0. X by BCIALG_1:def_5; then x0 <= x0 by BCIALG_1:def_11; then x0 in { yy2 where yy2 is Element of X : x0 <= yy2 } ; then x0 is Element of BranchV x0 ; then x0 \ a is Element of BranchV (x0 \ a) by A2, BCIALG_1:39; then (y \ b) \ (x0 \ a) is Element of BranchV a by A4, A5, BCIALG_1:39; then A6: (y \ b) \ (x0 \ a) <= ma by A1; y \ ((b * ((0. X) \ a)) * ma) = (y \ (b * ((0. X) \ a))) \ ma by Th12 .= ((y \ b) \ (x0 \ a)) \ ma by A3, Th12 .= 0. X by A6, BCIALG_1:def_11 ; hence y <= (b * ((0. X) \ a)) * ma by BCIALG_1:def_11; ::_thesis: verum end; hence ex mb being Element of X st for y being Element of BranchV b holds y <= mb ; ::_thesis: verum end; hence ex mb being Element of X st for y being Element of BranchV b holds y <= mb ; ::_thesis: verum end; 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 & 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 & y <= x * y ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: 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 let x, y be Element of X; ::_thesis: ( x <= x * y & y <= x * y ) A1: (x \ x) \ y = y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; A2: (y \ y) \ x = x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; A3: (x \ x) \ y = x \ (x * y) by Th12; (y \ y) \ x = y \ (y * x) by Th12 .= y \ (x * y) by Th7 ; hence ( x <= x * y & y <= x * y ) by A3, A1, A2, BCIALG_1:def_11; ::_thesis: verum end; hence for x, y being Element of X holds ( x <= x * y & y <= x * y ) ; ::_thesis: verum 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 proof let X be BCK-Algebra_with_Condition(S); ::_thesis: 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 let x, y, z be Element of X; ::_thesis: ((x * y) \ (y * z)) \ (z * x) = 0. X (y * x) \ y <= x by Lm2; then A1: ((y * x) \ y) \ z <= x \ z by BCIALG_1:5; x * y = y * x by Th7; then (x * y) \ (y * z) <= x \ z by A1, Th12; then A2: ((x * y) \ (y * z)) \ (z * x) <= (x \ z) \ (z * x) by BCIALG_1:5; (x \ z) \ (z * x) = ((x \ z) \ z) \ x by Th12 .= ((x \ z) \ x) \ z by BCIALG_1:7 .= ((x \ x) \ z) \ z by BCIALG_1:7 .= (z `) \ z by BCIALG_1:def_5 .= z ` by BCIALG_1:def_8 .= 0. X by BCIALG_1:def_8 ; then (((x * y) \ (y * z)) \ (z * x)) \ (0. X) = 0. X by A2, BCIALG_1:def_11; hence ((x * y) \ (y * z)) \ (z * x) = 0. X by BCIALG_1:2; ::_thesis: verum end; hence for x, y, z being Element of X holds ((x * y) \ (y * z)) \ (z * x) = 0. X ; ::_thesis: verum 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 proof let X be BCK-Algebra_with_Condition(S); ::_thesis: 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 let x, y be Element of X; ::_thesis: (x \ y) * (y \ x) <= x * y ((x \ y) * (y \ x)) \ (x \ y) <= y \ x by Lm2; then A1: (((x \ y) * (y \ x)) \ (x \ y)) \ y <= (y \ x) \ y by BCIALG_1:5; (y \ x) \ y = (y \ y) \ x by BCIALG_1:7 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then ((x \ y) * (y \ x)) \ ((x \ y) * y) <= 0. X by A1, Th12; then (((x \ y) * (y \ x)) \ ((x \ y) * y)) \ (0. X) = 0. X by BCIALG_1:def_11; then A2: ((x \ y) * (y \ x)) \ ((x \ y) * y) = 0. X by BCIALG_1:2; (y * (x \ y)) \ y <= x \ y by Lm2; then A3: ((y * (x \ y)) \ y) \ x <= (x \ y) \ x by BCIALG_1:5; (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then (y * (x \ y)) \ (y * x) <= 0. X by A3, Th12; then ((y * (x \ y)) \ (y * x)) \ (0. X) = 0. X by BCIALG_1:def_11; then A4: (y * (x \ y)) \ (y * x) = 0. X by BCIALG_1:2; (x \ y) * y = y * (x \ y) by Th7; then ((x \ y) * (y \ x)) \ (y * x) = 0. X by A2, A4, BCIALG_1:3; then (x \ y) * (y \ x) <= y * x by BCIALG_1:def_11; hence (x \ y) * (y \ x) <= x * y by Th7; ::_thesis: verum end; hence for x, y being Element of X holds (x \ y) * (y \ x) <= x * y ; ::_thesis: verum 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 proof let X be BCK-Algebra_with_Condition(S); ::_thesis: 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 let x be Element of X; ::_thesis: (x \ (0. X)) * ((0. X) \ x) = x A1: (0. X) \ x = x ` .= 0. X by BCIALG_1:def_8 ; x \ (0. X) = x by BCIALG_1:2; hence (x \ (0. X)) * ((0. X) \ x) = x by A1, Th9; ::_thesis: verum end; hence for x being Element of X holds (x \ (0. X)) * ((0. X) \ x) = x ; ::_thesis: verum end; 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 proof reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ; IT is commutative proof let x, y be Element of IT; :: according to BCIALG_4:def_9 ::_thesis: x \ (x \ y) = y \ (y \ x) thus x \ (x \ y) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum end; hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is commutative ; ::_thesis: verum end; 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) ) ) proof let X be non empty BCIStr_1 ; ::_thesis: ( 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) ) ) thus ( X is commutative BCK-Algebra_with_Condition(S) implies 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) ) ) ::_thesis: ( ( 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) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) proof assume A1: X is commutative BCK-Algebra_with_Condition(S) ; ::_thesis: 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) ) let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) (x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def9; then A2: (x \ z) \ (x \ y) = (y \ (y \ x)) \ z by A1, BCIALG_1:7 .= (y \ z) \ (y \ x) by A1, BCIALG_1:7 ; (0. X) \ y = y ` .= 0. X by A1, BCIALG_1:def_8 ; hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) by A1, A2, Th12, BCIALG_1:2; ::_thesis: verum end; thus ( ( 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) ) ) implies X is commutative BCK-Algebra_with_Condition(S) ) ::_thesis: verum proof assume A3: 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) ) ; ::_thesis: X is commutative BCK-Algebra_with_Condition(S) A4: for x, y being Element of X holds x \ (0. X) = x proof let x, y be Element of X; ::_thesis: x \ (0. X) = x (0. X) \ ((0. X) \ (0. X)) = 0. X by A3; hence x \ (0. X) = x by A3; ::_thesis: verum end; A5: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds x = y proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume ( x \ y = 0. X & y \ x = 0. X ) ; ::_thesis: x = y then (x \ (0. X)) \ (0. X) = (y \ (0. X)) \ (0. X) by A3; then x \ (0. X) = (y \ (0. X)) \ (0. X) by A4 .= y \ (0. X) by A4 ; hence x = y \ (0. X) by A4 .= y by A4 ; ::_thesis: verum end; A6: for x being Element of X holds x \ x = 0. X proof let x be Element of X; ::_thesis: x \ x = 0. X x = x \ (0. X) by A4; then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3 .= (0. X) \ ((0. X) \ x) by A4 .= 0. X by A3 ; hence x \ x = 0. X ; ::_thesis: verum end; A7: for x being Element of X holds (0. X) \ x = 0. X proof let x be Element of X; ::_thesis: (0. X) \ x = 0. X 0. X = ((0. X) \ x) \ ((0. X) \ x) by A6 .= (0. X) \ x by A3 ; hence (0. X) \ x = 0. X ; ::_thesis: verum end; A8: for x, y, z being Element of X holds ((x \ y) \ (x \ z)) \ (z \ y) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3 .= ((z \ y) \ (z \ x)) \ ((z \ y) \ (0. X)) by A4 .= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3 .= (0. X) \ ((0. X) \ (z \ y)) by A7 .= 0. X by A7 ; hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; ::_thesis: verum end; A9: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds x \ z = 0. X proof let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X ) assume that A10: x \ y = 0. X and A11: y \ z = 0. X ; ::_thesis: x \ z = 0. X ((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A8; then (x \ z) \ (x \ y) = 0. X by A4, A11; hence x \ z = 0. X by A4, A10; ::_thesis: verum end; A12: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ z) = 0. X by A8; then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ ((x \ (x \ z)) \ (z \ (0. X))) = 0. X by A4; then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (((x \ (0. X)) \ (x \ z)) \ (z \ (0. X))) = 0. X by A4; then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A8; then A13: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A4; ((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A8; hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A9, A13; ::_thesis: verum end; A14: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) x \ (x \ y) = (x \ ((0. X) \ y)) \ (x \ y) by A3 .= (y \ ((0. X) \ y)) \ (y \ x) by A3 .= y \ (y \ x) by A3 ; hence x \ (x \ y) = y \ (y \ x) ; ::_thesis: verum end; A15: for x, y, z being Element of X st x \ y = 0. X holds ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) proof let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X implies ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) ) assume A16: x \ y = 0. X ; ::_thesis: ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) ( ((z \ y) \ (z \ x)) \ (x \ y) = 0. X & ((x \ z) \ (x \ y)) \ (y \ z) = 0. X ) by A8; hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A4, A16; ::_thesis: verum end; A17: for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A8; then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A15; then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A15; then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A4; then (((x \ y) \ (z \ y)) \ (x \ z)) \ ((((x \ y) \ (0. X)) \ ((x \ y) \ (x \ z))) \ ((x \ z) \ (0. X))) = 0. X by A4; then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A8; hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A4; ::_thesis: verum end; for x being Element of X holds x ` = 0. X by A7; hence X is commutative BCK-Algebra_with_Condition(S) by A3, A6, A5, A14, A12, A17, Def2, Def9, BCIALG_1:def_3, BCIALG_1:def_4, BCIALG_1:def_5, BCIALG_1:def_7, BCIALG_1:def_8; ::_thesis: verum end; 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) proof let X be commutative BCK-Algebra_with_Condition(S); ::_thesis: 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) let a be Element of X; ::_thesis: ( a is greatest implies for x, y being Element of X holds x * y = a \ ((a \ x) \ y) ) assume A1: a is greatest ; ::_thesis: for x, y being Element of X holds x * y = a \ ((a \ x) \ y) for x, y being Element of X holds x * y = a \ ((a \ x) \ y) proof let x, y be Element of X; ::_thesis: x * y = a \ ((a \ x) \ y) A2: x * y <= a by A1, BCIALG_2:def_5; a \ ((a \ x) \ y) = a \ (a \ (x * y)) by Th12 .= (x * y) \ ((x * y) \ a) by Def9 .= (x * y) \ (0. X) by A2, BCIALG_1:def_11 ; hence x * y = a \ ((a \ x) \ y) by BCIALG_1:2; ::_thesis: verum end; hence for x, y being Element of X holds x * y = a \ ((a \ x) \ y) ; ::_thesis: verum end; 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 proof set Y = { t where t is Element of X : t <= a } ; A1: now__::_thesis:_for_y1_being_set_st_y1_in__{__t_where_t_is_Element_of_X_:_t_<=_a__}__holds_ y1_in_the_carrier_of_X let y1 be set ; ::_thesis: ( y1 in { t where t is Element of X : t <= a } implies y1 in the carrier of X ) assume y1 in { t where t is Element of X : t <= a } ; ::_thesis: y1 in the carrier of X then ex x1 being Element of X st ( y1 = x1 & x1 <= a ) ; hence y1 in the carrier of X ; ::_thesis: verum end; a \ a = 0. X by BCIALG_1:def_5; then a <= a by BCIALG_1:def_11; then a in { t where t is Element of X : t <= a } ; hence { t where t is Element of X : t <= a } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum end; 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) proof let X be commutative BCK-Algebra_with_Condition(S); ::_thesis: 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) let a, b, c be Element of X; ::_thesis: ( Condition_S (a,b) c= Initial_section c implies for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) ) assume A1: Condition_S (a,b) c= Initial_section c ; ::_thesis: for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) proof set u = c \ ((c \ a) \ b); let x be Element of Condition_S (a,b); ::_thesis: x <= c \ ((c \ a) \ b) A2: (c \ (c \ x)) \ x = (c \ x) \ (c \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; x in { t2 where t2 is Element of X : t2 <= c } by A1, TARSKI:def_3; then consider x2 being Element of X such that A3: x = x2 and A4: x2 <= c ; A5: x \ (c \ (c \ x)) = x \ (x \ (x \ c)) by Def9 .= x2 \ c by A3, BCIALG_1:8 .= 0. X by A4, BCIALG_1:def_11 ; then A6: ( ((c \ (c \ x)) \ (c \ ((c \ a) \ b))) \ (((c \ a) \ b) \ (c \ x)) = 0. X & x \ (c \ ((c \ a) \ b)) = (c \ (c \ x)) \ (c \ ((c \ a) \ b)) ) by A2, BCIALG_1:1, BCIALG_1:def_7; x in { t1 where t1 is Element of X : t1 \ a <= b } ; then A7: ex x1 being Element of X st ( x = x1 & x1 \ a <= b ) ; ((c \ a) \ b) \ (c \ x) = ((c \ a) \ (c \ x)) \ b by BCIALG_1:7 .= ((c \ (c \ x)) \ a) \ b by BCIALG_1:7 .= (x \ a) \ b by A5, A2, BCIALG_1:def_7 .= 0. X by A7, BCIALG_1:def_11 ; then x \ (c \ ((c \ a) \ b)) = 0. X by A6, BCIALG_1:2; hence x <= c \ ((c \ a) \ b) by BCIALG_1:def_11; ::_thesis: verum end; hence for x being Element of Condition_S (a,b) holds x <= c \ ((c \ a) \ b) ; ::_thesis: verum end; 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 proof reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ; IT is positive-implicative proof let x, y be Element of IT; :: according to BCIALG_4:def_11 ::_thesis: (x \ y) \ y = x \ y thus (x \ y) \ y = x \ y by STRUCT_0:def_10; ::_thesis: verum end; hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is positive-implicative ; ::_thesis: verum end; 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 ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x being Element of X holds x * x = x ) A1: ( X is positive-implicative implies for x being Element of X holds x * x = x ) proof assume A2: X is positive-implicative ; ::_thesis: for x being Element of X holds x * x = x let x be Element of X; ::_thesis: x * x = x A3: (x * x) \ x <= x by Lm2; (x * x) \ x = ((x * x) \ x) \ x by A2, Def11; then (x * x) \ x <= x \ x by A3, BCIALG_1:5; then ( x \ x = 0. X & ((x * x) \ x) \ (x \ x) = 0. X ) by BCIALG_1:def_5, BCIALG_1:def_11; then A4: (x * x) \ x = 0. X by BCIALG_1:2; x \ (x * x) = (x \ x) \ x by Th12 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x * x = x by A4, BCIALG_1:def_7; ::_thesis: verum end; ( ( for x being Element of X holds x * x = x ) implies X is positive-implicative ) proof assume A5: for x being Element of X holds x * x = x ; ::_thesis: X is positive-implicative for x, y being Element of X holds (x \ y) \ y = x \ y proof let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y x \ (y * y) = x \ y by A5; hence (x \ y) \ y = x \ y by Th12; ::_thesis: verum end; hence X is positive-implicative by Def11; ::_thesis: verum end; hence ( X is positive-implicative iff for x being Element of X holds x * x = x ) by A1; ::_thesis: verum end; 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 ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y being Element of X st x <= y holds x * y = y ) A1: ( X is positive-implicative implies for x, y being Element of X st x <= y holds x * y = y ) proof assume A2: X is positive-implicative ; ::_thesis: for x, y being Element of X st x <= y holds x * y = y let x, y be Element of X; ::_thesis: ( x <= y implies x * y = y ) A3: (y * x) \ y <= x by Lm2; (x * y) \ y = (y * x) \ y by Th7 .= ((y * x) \ y) \ y by A2, Def11 ; then (x * y) \ y <= x \ y by A3, BCIALG_1:5; then A4: ((x * y) \ y) \ (x \ y) = 0. X by BCIALG_1:def_11; A5: y \ (x * y) = y \ (y * x) by Th7 .= (y \ y) \ x by Th12 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; assume x <= y ; ::_thesis: x * y = y then x \ y = 0. X by BCIALG_1:def_11; then (x * y) \ y = 0. X by A4, BCIALG_1:2; hence x * y = y by A5, BCIALG_1:def_7; ::_thesis: verum end; ( ( for x, y being Element of X st x <= y holds x * y = y ) implies X is positive-implicative ) proof assume A6: for x, y being Element of X st x <= y holds x * y = y ; ::_thesis: X is positive-implicative for x being Element of X holds x * x = x proof let x be Element of X; ::_thesis: x * x = x x \ x = 0. X by BCIALG_1:def_5; then x <= x by BCIALG_1:def_11; hence x * x = x by A6; ::_thesis: verum end; hence X is positive-implicative by Th45; ::_thesis: verum end; hence ( X is positive-implicative iff for x, y being Element of X st x <= y holds x * y = y ) by A1; ::_thesis: verum end; 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) ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) A1: ( X is positive-implicative implies for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) proof assume A2: X is positive-implicative ; ::_thesis: for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) let x, y, z be Element of X; ::_thesis: (x * y) \ z = (x \ z) * (y \ z) (((x * y) \ z) \ (x \ z)) \ ((x * y) \ x) = 0. X by BCIALG_1:def_3; then ((x * y) \ z) \ (x \ z) <= (x * y) \ x by BCIALG_1:def_11; then (((x * y) \ z) \ (x \ z)) \ z <= ((x * y) \ x) \ z by BCIALG_1:5; then A3: ((((x * y) \ z) \ (x \ z)) \ z) \ (((x * y) \ x) \ z) = 0. X by BCIALG_1:def_11; (x * y) \ x <= y by Lm2; then ((x * y) \ x) \ z <= y \ z by BCIALG_1:5; then A4: (((x * y) \ x) \ z) \ (y \ z) = 0. X by BCIALG_1:def_11; (x * y) \ z = (x * y) \ (z * z) by A2, Th45 .= ((x * y) \ z) \ z by Th12 ; then ((x * y) \ z) \ (x \ z) = (((x * y) \ z) \ (x \ z)) \ z by BCIALG_1:7; then (((x * y) \ z) \ (x \ z)) \ (y \ z) = 0. X by A3, A4, BCIALG_1:3; then A5: ((x * y) \ z) \ ((x \ z) * (y \ z)) = 0. X by Th12; y <= x * y by Th38; then y \ z <= (x * y) \ z by BCIALG_1:5; then ((x * y) \ z) * (y \ z) <= ((x * y) \ z) * ((x * y) \ z) by Th8; then A6: (((x * y) \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by BCIALG_1:def_11; x <= x * y by Th38; then x \ z <= (x * y) \ z by BCIALG_1:5; then (x \ z) * (y \ z) <= ((x * y) \ z) * (y \ z) by Th8; then ((x \ z) * (y \ z)) \ (((x * y) \ z) * (y \ z)) = 0. X by BCIALG_1:def_11; then ((x \ z) * (y \ z)) \ (((x * y) \ z) * ((x * y) \ z)) = 0. X by A6, BCIALG_1:3; then ((x \ z) * (y \ z)) \ ((x * y) \ z) = 0. X by A2, Th45; hence (x * y) \ z = (x \ z) * (y \ z) by A5, BCIALG_1:def_7; ::_thesis: verum end; ( ( for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) implies X is positive-implicative ) proof assume A7: for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ; ::_thesis: X is positive-implicative for x being Element of X holds x * x = x proof let x be Element of X; ::_thesis: x * x = x (x * x) \ x = (x \ x) * (x \ x) by A7; then (x * x) \ x = (0. X) * (x \ x) by BCIALG_1:def_5; then (x * x) \ x = (0. X) * (0. X) by BCIALG_1:def_5; then A8: (x * x) \ x = 0. X by Th9; x \ (x * x) = (x \ x) \ x by Th12 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x * x = x by A8, BCIALG_1:def_7; ::_thesis: verum end; hence X is positive-implicative by Th45; ::_thesis: verum end; hence ( X is positive-implicative iff for x, y, z being Element of X holds (x * y) \ z = (x \ z) * (y \ z) ) by A1; ::_thesis: verum end; 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) ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) ) A1: ( X is positive-implicative implies for x, y being Element of X holds x * y = x * (y \ x) ) proof assume A2: X is positive-implicative ; ::_thesis: for x, y being Element of X holds x * y = x * (y \ x) let x, y be Element of X; ::_thesis: x * y = x * (y \ x) (y \ x) \ y = (y \ y) \ x by BCIALG_1:7 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then y \ x <= y by BCIALG_1:def_11; then x * (y \ x) <= x * y by Th8; then A3: (x * (y \ x)) \ (x * y) = 0. X by BCIALG_1:def_11; (x * y) \ x = (x \ x) * (y \ x) by A2, Th47 .= (0. X) * (y \ x) by BCIALG_1:def_5 .= y \ x by Th9 ; then ((x * y) \ x) \ (y \ x) = 0. X by BCIALG_1:def_5; then (x * y) \ (x * (y \ x)) = 0. X by Th12; hence x * y = x * (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum end; ( ( for x, y being Element of X holds x * y = x * (y \ x) ) implies X is positive-implicative ) proof assume A4: for x, y being Element of X holds x * y = x * (y \ x) ; ::_thesis: X is positive-implicative for x, y being Element of X holds (x \ y) \ y = x \ y proof let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y y * y = y * (y \ y) by A4 .= y * (0. X) by BCIALG_1:def_5 .= y by Th9 ; hence (x \ y) \ y = x \ y by Th12; ::_thesis: verum end; hence X is positive-implicative by Def11; ::_thesis: verum end; hence ( X is positive-implicative iff for x, y being Element of X holds x * y = x * (y \ x) ) by A1; ::_thesis: verum end; 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)) proof let X be positive-implicative BCK-Algebra_with_Condition(S); ::_thesis: 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 let x, y be Element of X; ::_thesis: x = (x \ y) * (x \ (x \ y)) (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ y <= x by BCIALG_1:def_11; then x = (x \ y) * x by Th46; hence x = (x \ y) * (x \ (x \ y)) by Th48; ::_thesis: verum end; hence for x, y being Element of X holds x = (x \ y) * (x \ (x \ y)) ; ::_thesis: verum end; 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 & 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 ) proof thus BCI_S-EXAMPLE is being_SB-1 ::_thesis: ( 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 ) proof let x be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_12 ::_thesis: x * x = x thus x * x = x by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_SB-2 ::_thesis: ( BCI_S-EXAMPLE is being_SB-4 & BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S ) proof let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_13 ::_thesis: x * y = y * x thus x * y = y * x by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_SB-4 ::_thesis: ( BCI_S-EXAMPLE is being_I & BCI_S-EXAMPLE is with_condition_S ) proof let x, y be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_14 ::_thesis: (x \ y) * y = x * y thus (x \ y) * y = x * y by STRUCT_0:def_10; ::_thesis: verum end; thus BCI_S-EXAMPLE is being_I ; ::_thesis: BCI_S-EXAMPLE is with_condition_S let x, y, z be Element of BCI_S-EXAMPLE; :: according to BCIALG_4:def_2 ::_thesis: (x \ y) \ z = x \ (y * z) thus (x \ y) \ z = x \ (y * z) by STRUCT_0:def_10; ::_thesis: verum end; 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 & 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; 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 & b1 is being_SB-1 & b1 is being_SB-2 & b1 is being_SB-4 & b1 is being_I & 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 ) proof let X be non empty BCIStr_1 ; ::_thesis: ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra ) A1: ( X is semi-Brouwerian-algebra implies X is positive-implicative BCK-Algebra_with_Condition(S) ) proof assume A2: X is semi-Brouwerian-algebra ; ::_thesis: X is positive-implicative BCK-Algebra_with_Condition(S) A3: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds x = y proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume that A4: x \ y = 0. X and A5: y \ x = 0. X ; ::_thesis: x = y A6: x = x * x by A2, Def12 .= (x \ x) * x by A2, Def14 .= (0. X) * x by A2, BCIALG_1:def_5 .= y * x by A2, A5, Def14 ; y = y * y by A2, Def12 .= (y \ y) * y by A2, Def14 .= y * (y \ y) by A2, Def13 .= y * (0. X) by A2, BCIALG_1:def_5 .= (x \ y) * y by A2, A4, Def13 .= x * y by A2, Def14 ; hence x = y by A2, A6, Def13; ::_thesis: verum end; A7: for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ y (x \ y) \ z = x \ (y * z) by A2, Def2 .= x \ (z * y) by A2, Def13 ; hence (x \ y) \ z = (x \ z) \ y by A2, Def2; ::_thesis: verum end; A8: for x, y, z being Element of X holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. X ((x \ y) \ z) \ ((x \ z) \ y) = ((x \ y) \ z) \ ((x \ y) \ z) by A7; hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A2, BCIALG_1:def_5; ::_thesis: verum end; A9: for x, y being Element of X holds x * y = x * (y \ x) proof let x, y be Element of X; ::_thesis: x * y = x * (y \ x) x * (y \ x) = (y \ x) * x by A2, Def13 .= y * x by A2, Def14 ; hence x * y = x * (y \ x) by A2, Def13; ::_thesis: verum end; A10: for x being Element of X holds x ` = 0. X proof let x be Element of X; ::_thesis: x ` = 0. X (0. X) \ x = (x \ x) \ x by A2, BCIALG_1:def_5 .= x \ (x * x) by A2, Def2 .= x \ x by A2, Def12 .= 0. X by A2, BCIALG_1:def_5 ; hence x ` = 0. X ; ::_thesis: verum end; for x, y, z being Element of X holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X ((x \ y) \ (z \ y)) \ (x \ z) = (x \ (y * (z \ y))) \ (x \ z) by A2, Def2 .= (x \ ((z \ y) * y)) \ (x \ z) by A2, Def13 .= (x \ (z * y)) \ (x \ z) by A2, Def14 .= ((x \ z) \ y) \ (x \ z) by A2, Def2 .= ((x \ z) \ (x \ z)) \ y by A7 .= y ` by A2, BCIALG_1:def_5 ; hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A10; ::_thesis: verum end; hence X is positive-implicative BCK-Algebra_with_Condition(S) by A2, A10, A3, A8, A9, Th48, BCIALG_1:def_3, BCIALG_1:def_4, BCIALG_1:def_7, BCIALG_1:def_8; ::_thesis: verum end; ( X is positive-implicative BCK-Algebra_with_Condition(S) implies X is semi-Brouwerian-algebra ) proof assume A11: X is positive-implicative BCK-Algebra_with_Condition(S) ; ::_thesis: X is semi-Brouwerian-algebra A12: for x, y being Element of X holds (x \ y) * y = x * y proof let x, y be Element of X; ::_thesis: (x \ y) * y = x * y y * x = y * (x \ y) by A11, Th48; then x * y = y * (x \ y) by A11, Th7; hence (x \ y) * y = x * y by A11, Th7; ::_thesis: verum end; ( ( for x being Element of X holds x * x = x ) & ( for x, y being Element of X holds x * y = y * x ) ) by A11, Th7, Th45; hence X is semi-Brouwerian-algebra by A11, A12, Def12, Def13, Def14; ::_thesis: verum end; hence ( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra ) by A1; ::_thesis: verum end; 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 proof reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ; IT is implicative proof let x, y be Element of IT; :: according to BCIALG_4:def_15 ::_thesis: x \ (y \ x) = x thus x \ (y \ x) = x by STRUCT_0:def_10; ::_thesis: verum end; hence ex b1 being BCK-Algebra_with_Condition(S) st b1 is implicative ; ::_thesis: verum end; end; theorem Th51: :: BCIALG_4:51 for X being BCK-Algebra_with_Condition(S) holds ( X is implicative iff ( X is commutative & X is positive-implicative ) ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is implicative iff ( X is commutative & X is positive-implicative ) ) thus ( X is implicative implies ( X is commutative & X is positive-implicative ) ) ::_thesis: ( X is commutative & X is positive-implicative implies X is implicative ) proof assume A1: X is implicative ; ::_thesis: ( X is commutative & X is positive-implicative ) A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then x \ (x \ y) <= y by BCIALG_1:def_11; then (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5; then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7; hence x \ (x \ y) <= y \ (y \ x) by A1, Def15; ::_thesis: verum end; A3: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) y \ (y \ x) <= x \ (x \ y) by A2; then A4: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by BCIALG_1:def_11; x \ (x \ y) <= y \ (y \ x) by A2; then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def_11; hence x \ (x \ y) = y \ (y \ x) by A4, BCIALG_1:def_7; ::_thesis: verum end; for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y (x \ y) \ (y \ (x \ y)) = x \ y by A1, Def15; hence x \ y = (x \ y) \ y by A1, Def15; ::_thesis: verum end; hence ( X is commutative & X is positive-implicative ) by A3, Def9, Def11; ::_thesis: verum end; assume that A5: X is commutative and A6: X is positive-implicative ; ::_thesis: X is implicative for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8; then A7: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A5, Def9; (y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A6, Def11 .= 0. X by BCIALG_1:def_5 ; hence x \ (y \ x) = x by A7, BCIALG_1:2; ::_thesis: verum end; hence X is implicative by Def15; ::_thesis: verum 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)) ) proof let X be BCK-Algebra_with_Condition(S); ::_thesis: ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) A1: ( X is implicative implies for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) proof assume A2: X is implicative ; ::_thesis: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) then A3: X is positive-implicative by Th51; let x, y, z be Element of X; ::_thesis: x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) A4: X is commutative by A2, Th51; x = (x \ z) * (x \ (x \ z)) by A3, Th49; then A5: x \ (y \ z) = ((x \ z) * (z \ (z \ x))) \ (y \ z) by A4, Def9; (y \ z) \ y = (y \ y) \ z by BCIALG_1:7 .= z ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then y \ z <= y by BCIALG_1:def_11; then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5; then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:def_11; then A6: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7; ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A3, Def11 .= (((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_3 ; then A7: (x \ y) \ z = (x \ z) \ (y \ z) by A6, BCIALG_1:def_7; (z \ (z \ x)) \ (y \ z) = (z \ (y \ z)) \ (z \ x) by BCIALG_1:7 .= z \ (z \ x) by A2, Def15 ; hence x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) by A3, A5, A7, Th47; ::_thesis: verum end; ( ( for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) implies X is implicative ) proof assume A8: for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ; ::_thesis: X is implicative for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x x \ (y \ x) = ((x \ y) \ x) * (x \ (x \ x)) by A8 .= ((x \ y) \ x) * (x \ (0. X)) by BCIALG_1:def_5 .= ((x \ y) \ x) * x by BCIALG_1:2 .= ((x \ x) \ y) * x by BCIALG_1:7 .= (y `) * x by BCIALG_1:def_5 .= (0. X) * x by BCIALG_1:def_8 ; hence x \ (y \ x) = x by Th9; ::_thesis: verum end; hence X is implicative by Def15; ::_thesis: verum end; hence ( X is implicative iff for x, y, z being Element of X holds x \ (y \ z) = ((x \ y) \ z) * (z \ (z \ x)) ) by A1; ::_thesis: verum end;