:: BCIALG_1 semantic presentation begin definition attrc1 is strict ; struct BCIStr -> 1-sorted ; aggrBCIStr(# carrier, InternalDiff #) -> BCIStr ; sel InternalDiff c1 -> BinOp of the carrier of c1; end; registration cluster non empty strict for BCIStr ; existence ex b1 being BCIStr st ( not b1 is empty & b1 is strict ) proof set A = the non empty set ; set m = the BinOp of the non empty set ; take BCIStr(# the non empty set , the BinOp of the non empty set #) ; ::_thesis: ( not BCIStr(# the non empty set , the BinOp of the non empty set #) is empty & BCIStr(# the non empty set , the BinOp of the non empty set #) is strict ) thus not the carrier of BCIStr(# the non empty set , the BinOp of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: BCIStr(# the non empty set , the BinOp of the non empty set #) is strict thus BCIStr(# the non empty set , the BinOp of the non empty set #) is strict ; ::_thesis: verum end; end; definition let A be BCIStr ; let x, y be Element of A; funcx \ y -> Element of A equals :: BCIALG_1:def 1 the InternalDiff of A . (x,y); coherence the InternalDiff of A . (x,y) is Element of A ; end; :: deftheorem defines \ BCIALG_1:def_1_:_ for A being BCIStr for x, y being Element of A holds x \ y = the InternalDiff of A . (x,y); definition attrc1 is strict ; struct BCIStr_0 -> BCIStr , ZeroStr ; aggrBCIStr_0(# carrier, InternalDiff, ZeroF #) -> BCIStr_0 ; end; registration cluster non empty strict for BCIStr_0 ; existence ex b1 being BCIStr_0 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_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) ; ::_thesis: ( not BCIStr_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is empty & BCIStr_0(# 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_0(# 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_0(# the non empty set , the BinOp of the non empty set , the Element of the non empty set #) is strict thus BCIStr_0(# 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 IT be non empty BCIStr_0 ; let x be Element of IT; funcx ` -> Element of IT equals :: BCIALG_1:def 2 (0. IT) \ x; coherence (0. IT) \ x is Element of IT ; end; :: deftheorem defines ` BCIALG_1:def_2_:_ for IT being non empty BCIStr_0 for x being Element of IT holds x ` = (0. IT) \ x; definition let IT be non empty BCIStr_0 ; attrIT is being_B means :Def3: :: BCIALG_1:def 3 for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT; attrIT is being_C means :Def4: :: BCIALG_1:def 4 for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT; attrIT is being_I means :Def5: :: BCIALG_1:def 5 for x being Element of IT holds x \ x = 0. IT; attrIT is being_K means :Def6: :: BCIALG_1:def 6 for x, y being Element of IT holds (x \ y) \ x = 0. IT; attrIT is being_BCI-4 means :Def7: :: BCIALG_1:def 7 for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds x = y; attrIT is being_BCK-5 means :Def8: :: BCIALG_1:def 8 for x being Element of IT holds x ` = 0. IT; end; :: deftheorem Def3 defines being_B BCIALG_1:def_3_:_ for IT being non empty BCIStr_0 holds ( IT is being_B iff for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT ); :: deftheorem Def4 defines being_C BCIALG_1:def_4_:_ for IT being non empty BCIStr_0 holds ( IT is being_C iff for x, y, z being Element of IT holds ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT ); :: deftheorem Def5 defines being_I BCIALG_1:def_5_:_ for IT being non empty BCIStr_0 holds ( IT is being_I iff for x being Element of IT holds x \ x = 0. IT ); :: deftheorem Def6 defines being_K BCIALG_1:def_6_:_ for IT being non empty BCIStr_0 holds ( IT is being_K iff for x, y being Element of IT holds (x \ y) \ x = 0. IT ); :: deftheorem Def7 defines being_BCI-4 BCIALG_1:def_7_:_ for IT being non empty BCIStr_0 holds ( IT is being_BCI-4 iff for x, y being Element of IT st x \ y = 0. IT & y \ x = 0. IT holds x = y ); :: deftheorem Def8 defines being_BCK-5 BCIALG_1:def_8_:_ for IT being non empty BCIStr_0 holds ( IT is being_BCK-5 iff for x being Element of IT holds x ` = 0. IT ); definition func BCI-EXAMPLE -> BCIStr_0 equals :: BCIALG_1:def 9 BCIStr_0(# 1,op2,op0 #); coherence BCIStr_0(# 1,op2,op0 #) is BCIStr_0 ; end; :: deftheorem defines BCI-EXAMPLE BCIALG_1:def_9_:_ BCI-EXAMPLE = BCIStr_0(# 1,op2,op0 #); registration cluster BCI-EXAMPLE -> 1 -element strict ; coherence ( BCI-EXAMPLE is strict & BCI-EXAMPLE is 1 -element ) by CARD_1:49, STRUCT_0:def_19; end; registration cluster BCI-EXAMPLE -> being_B being_C being_I being_BCI-4 being_BCK-5 ; coherence ( BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) proof thus BCI-EXAMPLE is being_B ::_thesis: ( BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) proof let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_3 ::_thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE thus ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI-EXAMPLE is being_C ::_thesis: ( BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) proof let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_4 ::_thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE thus ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI-EXAMPLE is being_I ::_thesis: ( BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) proof let x be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. BCI-EXAMPLE thus x \ x = 0. BCI-EXAMPLE by STRUCT_0:def_10; ::_thesis: verum end; thus BCI-EXAMPLE is being_BCI-4 ::_thesis: BCI-EXAMPLE is being_BCK-5 proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_7 ::_thesis: ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y ) thus ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y ) by STRUCT_0:def_10; ::_thesis: verum end; for x being Element of BCI-EXAMPLE holds x ` = 0. BCI-EXAMPLE by STRUCT_0:def_10; hence BCI-EXAMPLE is being_BCK-5 by Def8; ::_thesis: verum end; end; registration cluster non empty strict being_B being_C being_I being_BCI-4 being_BCK-5 for BCIStr_0 ; existence ex b1 being non empty BCIStr_0 st ( b1 is strict & b1 is being_B & b1 is being_C & b1 is being_I & b1 is being_BCI-4 & b1 is being_BCK-5 ) proof take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) thus ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) ; ::_thesis: verum end; end; definition mode BCI-algebra is non empty being_B being_C being_I being_BCI-4 BCIStr_0 ; end; definition mode BCK-algebra is being_BCK-5 BCI-algebra; end; definition let X be BCI-algebra; mode SubAlgebra of X -> BCI-algebra means :Def10: :: BCIALG_1:def 10 ( 0. it = 0. X & the carrier of it c= the carrier of X & the InternalDiff of it = the InternalDiff of X || the carrier of it ); existence ex b1 being BCI-algebra st ( 0. b1 = 0. X & the carrier of b1 c= the carrier of X & the InternalDiff of b1 = the InternalDiff of X || the carrier of b1 ) proof take X ; ::_thesis: ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1; hence ( 0. X = 0. X & the carrier of X c= the carrier of X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) by RELAT_1:68; ::_thesis: verum end; end; :: deftheorem Def10 defines SubAlgebra BCIALG_1:def_10_:_ for X, b2 being BCI-algebra holds ( b2 is SubAlgebra of X iff ( 0. b2 = 0. X & the carrier of b2 c= the carrier of X & the InternalDiff of b2 = the InternalDiff of X || the carrier of b2 ) ); theorem Th1: :: BCIALG_1:1 for X being non empty BCIStr_0 holds ( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-algebra iff ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ) thus ( X is BCI-algebra implies ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) ) ::_thesis: ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) implies X is BCI-algebra ) proof assume A1: X is BCI-algebra ; ::_thesis: ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_x_\_x_=_0._X_&_(_x_\_y_=_0._X_&_y_\_x_=_0._X_implies_x_=_y_)_) let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) ) A2: ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A1, Def3; A3: 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 \ z) \ y) = 0. X & ((x \ z) \ y) \ ((x \ y) \ z) = 0. X ) by A1, Def4; hence (x \ y) \ z = (x \ z) \ y by A1, Def7; ::_thesis: verum end; then (x \ (x \ y)) \ y = (x \ y) \ (x \ y) ; hence ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & x \ x = 0. X & ( x \ y = 0. X & y \ x = 0. X implies x = y ) ) by A1, A2, A3, Def5, Def7; ::_thesis: verum end; hence ( X is being_I & X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ) ) by A1; ::_thesis: verum end; assume that A4: X is being_I and A5: X is being_BCI-4 and A6: for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ; ::_thesis: X is BCI-algebra A7: for x being Element of X st x \ (0. X) = 0. X holds x = 0. X proof let x be Element of X; ::_thesis: ( x \ (0. X) = 0. X implies x = 0. X ) assume A8: x \ (0. X) = 0. X ; ::_thesis: x = 0. X then x ` = (x \ (x \ x)) \ x by A4, Def5 .= 0. X by A6 ; hence x = 0. X by A5, A8, Def7; ::_thesis: verum end; A9: for x being Element of X holds x \ (0. X) = x proof let x be Element of X; ::_thesis: x \ (0. X) = x (x \ (x \ (0. X))) \ (0. X) = 0. X by A6; then A10: x \ (x \ (0. X)) = 0. X by A7; 0. X = (x \ (x \ x)) \ x by A6 .= (x \ (0. X)) \ x by A4, Def5 ; hence x \ (0. X) = x by A5, A10, Def7; ::_thesis: verum end; A11: 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 A12: x \ y = 0. X and A13: y \ z = 0. X ; ::_thesis: x \ z = 0. X ((x \ z) \ (x \ y)) \ (y \ z) = 0. X by A6; then (x \ z) \ (x \ y) = 0. X by A9, A13; hence x \ z = 0. X by A9, A12; ::_thesis: verum end; A14: 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 A6; then (((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z)))) \ (0. X) = 0. X by A6; then A15: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by A7; ((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by A6; hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A11, A15; ::_thesis: verum end; A16: 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 A17: 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 A6; hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A9, A17; ::_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) \ (x \ z)) \ (z \ y) = 0. X by A6; then ((x \ y) \ (z \ y)) \ ((x \ y) \ ((x \ y) \ (x \ z))) = 0. X by A16; then (((x \ y) \ (z \ y)) \ (x \ z)) \ (((x \ y) \ ((x \ y) \ (x \ z))) \ (x \ z)) = 0. X by A16; then (((x \ y) \ (z \ y)) \ (x \ z)) \ (0. X) = 0. X by A6; hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. X by A7; ::_thesis: verum end; hence X is BCI-algebra by A4, A5, A14, Def3, Def4; ::_thesis: verum end; definition let IT be non empty BCIStr_0 ; let x, y be Element of IT; predx <= y means :Def11: :: BCIALG_1:def 11 x \ y = 0. IT; end; :: deftheorem Def11 defines <= BCIALG_1:def_11_:_ for IT being non empty BCIStr_0 for x, y being Element of IT holds ( x <= y iff x \ y = 0. IT ); Lm1: for X being BCI-algebra for x being Element of X st x \ (0. X) = 0. X holds x = 0. X proof let X be BCI-algebra; ::_thesis: for x being Element of X st x \ (0. X) = 0. X holds x = 0. X let x be Element of X; ::_thesis: ( x \ (0. X) = 0. X implies x = 0. X ) assume A1: x \ (0. X) = 0. X ; ::_thesis: x = 0. X then x ` = (x \ (x \ x)) \ x by Def5 .= 0. X by Th1 ; hence x = 0. X by A1, Def7; ::_thesis: verum end; theorem Th2: :: BCIALG_1:2 for X being BCI-algebra for x being Element of X holds x \ (0. X) = x proof let X be BCI-algebra; ::_thesis: for x being Element of X holds x \ (0. X) = x let x be Element of X; ::_thesis: x \ (0. X) = x (x \ (x \ (0. X))) \ (0. X) = 0. X by Th1; then A1: x \ (x \ (0. X)) = 0. X by Lm1; 0. X = (x \ (x \ x)) \ x by Th1 .= (x \ (0. X)) \ x by Def5 ; hence x \ (0. X) = x by A1, Def7; ::_thesis: verum end; theorem Th3: :: BCIALG_1:3 for X being BCI-algebra 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 be BCI-algebra; ::_thesis: for x, y, z being Element of X st x \ y = 0. X & y \ z = 0. X holds x \ z = 0. X let x, y, z be Element of X; ::_thesis: ( x \ y = 0. X & y \ z = 0. X implies x \ z = 0. X ) assume that A1: x \ y = 0. X and A2: y \ z = 0. X ; ::_thesis: x \ z = 0. X ((x \ z) \ (x \ y)) \ (y \ z) = 0. X by Th1; then (x \ z) \ (x \ y) = 0. X by A2, Th2; hence x \ z = 0. X by A1, Th2; ::_thesis: verum end; theorem Th4: :: BCIALG_1:4 for X being BCI-algebra 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 be BCI-algebra; ::_thesis: 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 ) 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 A1: 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 Th1; hence ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by A1, Th2; ::_thesis: verum end; theorem :: BCIALG_1:5 for X being BCI-algebra for x, y, z being Element of X st x <= y holds ( x \ z <= y \ z & z \ y <= z \ x ) proof let X be BCI-algebra; ::_thesis: for x, y, z being Element of X st x <= y holds ( x \ z <= y \ z & z \ y <= z \ x ) let x, y, z be Element of X; ::_thesis: ( x <= y implies ( x \ z <= y \ z & z \ y <= z \ x ) ) assume x <= y ; ::_thesis: ( x \ z <= y \ z & z \ y <= z \ x ) then x \ y = 0. X by Def11; then ( (x \ z) \ (y \ z) = 0. X & (z \ y) \ (z \ x) = 0. X ) by Th4; hence ( x \ z <= y \ z & z \ y <= z \ x ) by Def11; ::_thesis: verum end; theorem :: BCIALG_1:6 for X being BCI-algebra for x, y being Element of X st x \ y = 0. X holds (y \ x) ` = 0. X proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st x \ y = 0. X holds (y \ x) ` = 0. X let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies (y \ x) ` = 0. X ) assume x \ y = 0. X ; ::_thesis: (y \ x) ` = 0. X then (x \ x) \ (y \ x) = 0. X by Th4; hence (y \ x) ` = 0. X by Def5; ::_thesis: verum end; theorem Th7: :: BCIALG_1:7 for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y proof let X be BCI-algebra; ::_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 \ (x \ z)) \ z = 0. X by Th1; then A1: ((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X by Th4; (x \ (x \ y)) \ y = 0. X by Th1; then A2: ((x \ z) \ y) \ ((x \ z) \ (x \ (x \ y))) = 0. X by Th4; ((x \ z) \ (x \ (x \ y))) \ ((x \ y) \ z) = 0. X by Th1; then A3: ((x \ z) \ y) \ ((x \ y) \ z) = 0. X by A2, Th3; ((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X by Th1; then ((x \ y) \ z) \ ((x \ z) \ y) = 0. X by A1, Th3; hence (x \ y) \ z = (x \ z) \ y by A3, Def7; ::_thesis: verum end; theorem Th8: :: BCIALG_1:8 for X being BCI-algebra for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y proof let X be BCI-algebra; ::_thesis: for x, y being Element of X holds x \ (x \ (x \ y)) = x \ y let x, y be Element of X; ::_thesis: x \ (x \ (x \ y)) = x \ y ((x \ y) \ (x \ (x \ (x \ y)))) \ ((x \ (x \ y)) \ y) = 0. X by Th1; then ((x \ y) \ (x \ (x \ (x \ y)))) \ (0. X) = 0. X by Th1; then A1: (x \ y) \ (x \ (x \ (x \ y))) = 0. X by Th2; (x \ (x \ (x \ y))) \ (x \ y) = 0. X by Th1; hence x \ (x \ (x \ y)) = x \ y by A1, Def7; ::_thesis: verum end; theorem Th9: :: BCIALG_1:9 for X being BCI-algebra for x, y being Element of X holds (x \ y) ` = (x `) \ (y `) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X holds (x \ y) ` = (x `) \ (y `) let x, y be Element of X; ::_thesis: (x \ y) ` = (x `) \ (y `) (x `) \ (y `) = (((x \ y) \ (x \ y)) \ x) \ (y `) by Def5 .= (((x \ y) \ x) \ (x \ y)) \ (y `) by Th7 .= (((x \ x) \ y) \ (x \ y)) \ (y `) by Th7 .= ((y `) \ (x \ y)) \ (y `) by Def5 .= ((y `) \ (y `)) \ (x \ y) by Th7 ; hence (x \ y) ` = (x `) \ (y `) by Def5; ::_thesis: verum end; theorem Th10: :: BCIALG_1:10 for X being BCI-algebra for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X proof let X be BCI-algebra; ::_thesis: for x, y being Element of X holds ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X let x, y be Element of X; ::_thesis: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) by Th7 .= ((x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y)) \ (y \ x) by Th7 .= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ x) by Th8 .= ((x \ (y \ (y \ x))) \ (x \ y)) \ (y \ (y \ (y \ x))) by Th8 ; hence ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th1; ::_thesis: verum end; theorem :: BCIALG_1:11 for X being non empty BCIStr_0 holds ( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-algebra iff ( X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) ) thus ( X is BCI-algebra implies ( X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) ) ) by Th1, Th2; ::_thesis: ( X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra ) thus ( X is being_BCI-4 & ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ) implies X is BCI-algebra ) ::_thesis: verum proof assume that A1: X is being_BCI-4 and A2: for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x ) ; ::_thesis: X is BCI-algebra A3: X is being_I proof let x be Element of X; :: according to BCIALG_1:def_5 ::_thesis: x \ x = 0. X x \ x = (x \ x) \ (0. X) by A2; then x \ x = ((x \ (0. X)) \ x) \ (0. X) by A2; then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A2; then x \ x = ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A2; hence x \ x = 0. X by A2; ::_thesis: verum end; now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_) let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A2; then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A2; hence ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) by A2; ::_thesis: verum end; hence X is BCI-algebra by A1, A3, Th1; ::_thesis: verum end; end; theorem :: BCIALG_1:12 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCK-algebra for z being Element of X holds z ` = 0. X proof let z be Element of X; ::_thesis: z ` = 0. X (z `) ` = z \ (z \ (0. X)) by A1; then (z `) ` = z \ z by Th2; then ((z `) `) \ z = z ` by Def5; hence z ` = 0. X by Th1; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:13 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y being Element of X holds (x \ y) \ y = x \ y ; ::_thesis: X is BCK-algebra for z being Element of X holds z ` = 0. X proof let z be Element of X; ::_thesis: z ` = 0. X (z `) \ ((z `) \ z) = (z `) \ (z `) by A1; then (z `) \ ((z `) \ z) = 0. X by Def5; hence z ` = 0. X by Th1; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:14 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y being Element of X holds x \ (y \ x) = x ; ::_thesis: X is BCK-algebra for z being Element of X holds z ` = 0. X proof let z be Element of X; ::_thesis: z ` = 0. X (z \ (0. X)) ` = 0. X by A1; hence z ` = 0. X by Th2; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:15 for X being BCI-algebra st ( for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; ::_thesis: X is BCK-algebra for s being Element of X holds s ` = 0. X proof let s be Element of X; ::_thesis: s ` = 0. X (s `) \ s = (s `) \ (s \ s) by A1; then (s `) \ s = (s `) \ (0. X) by Def5; then (s `) \ ((s `) \ s) = (s `) \ (s `) by Th2; then (s `) \ ((s `) \ s) = 0. X by Def5; hence s ` = 0. X by Th1; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:16 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y being Element of X holds (x \ y) \ (y \ x) = x \ y ; ::_thesis: X is BCK-algebra for s being Element of X holds s ` = 0. X proof let s be Element of X; ::_thesis: s ` = 0. X (s `) \ (s \ (0. X)) = s ` by A1; then (s `) \ ((s `) \ s) = (s `) \ (s `) by Th2; then (s `) \ ((s `) \ s) = 0. X by Def5; hence s ` = 0. X by Th1; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:17 for X being BCI-algebra st ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ( for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies X is BCK-algebra ) assume A1: for X being BCI-algebra for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; ::_thesis: X is BCK-algebra for s being Element of X holds s ` = 0. X proof let s be Element of X; ::_thesis: s ` = 0. X (s `) \ ((s `) \ (s \ (0. X))) = 0. X by A1; then ((s `) \ ((s `) \ s)) \ s = s ` by Th2; hence s ` = 0. X by Th1; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; theorem :: BCIALG_1:18 for X being BCI-algebra holds ( X is being_K iff X is BCK-algebra ) proof let X be BCI-algebra; ::_thesis: ( X is being_K iff X is BCK-algebra ) thus ( X is being_K implies X is BCK-algebra ) ::_thesis: ( X is BCK-algebra implies X is being_K ) proof assume A1: X is being_K ; ::_thesis: X is BCK-algebra now__::_thesis:_for_s_being_Element_of_X_holds_s_`_=_0._X let s be Element of X; ::_thesis: s ` = 0. X (s `) \ (0. X) = 0. X by A1, Def6; hence s ` = 0. X by Th2; ::_thesis: verum end; hence X is BCK-algebra by Def8; ::_thesis: verum end; assume A2: X is BCK-algebra ; ::_thesis: X is being_K let x, y be Element of X; :: according to BCIALG_1:def_6 ::_thesis: (x \ y) \ x = 0. X y ` = 0. X by A2, Def8; then (x \ y) \ (x \ (0. X)) = 0. X by Th4; hence (x \ y) \ x = 0. X by Th2; ::_thesis: verum end; definition let X be BCI-algebra; func BCK-part X -> non empty Subset of X equals :: BCIALG_1:def 12 { x where x is Element of X : 0. X <= x } ; coherence { x where x is Element of X : 0. X <= x } is non empty Subset of X proof set Y = { x where x is Element of X : 0. X <= x } ; A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_0._X_<=_x__}__holds_ y_in_the_carrier_of_X let y be set ; ::_thesis: ( y in { x where x is Element of X : 0. X <= x } implies y in the carrier of X ) assume y in { x where x is Element of X : 0. X <= x } ; ::_thesis: y in the carrier of X then ex x being Element of X st ( y = x & 0. X <= x ) ; hence y in the carrier of X ; ::_thesis: verum end; (0. X) ` = 0. X by Def5; then 0. X <= 0. X by Def11; then 0. X in { x where x is Element of X : 0. X <= x } ; hence { x where x is Element of X : 0. X <= x } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines BCK-part BCIALG_1:def_12_:_ for X being BCI-algebra holds BCK-part X = { x where x is Element of X : 0. X <= x } ; theorem Th19: :: BCIALG_1:19 for X being BCI-algebra holds 0. X in BCK-part X proof let X be BCI-algebra; ::_thesis: 0. X in BCK-part X (0. X) ` = 0. X by Def5; then 0. X <= 0. X by Def11; hence 0. X in BCK-part X ; ::_thesis: verum end; theorem :: BCIALG_1:20 for X being BCI-algebra for x, y being Element of BCK-part X holds x \ y in BCK-part X proof let X be BCI-algebra; ::_thesis: for x, y being Element of BCK-part X holds x \ y in BCK-part X let x, y be Element of BCK-part X; ::_thesis: x \ y in BCK-part X x in { x1 where x1 is Element of X : 0. X <= x1 } ; then A1: ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) ; y in { y1 where y1 is Element of X : 0. X <= y1 } ; then A2: ex y1 being Element of X st ( y = y1 & 0. X <= y1 ) ; (x \ y) ` = (x `) \ (y `) by Th9; then (x \ y) ` = (y `) ` by A1, Def11; then (x \ y) ` = (0. X) ` by A2, Def11; then (x \ y) ` = 0. X by Def5; then 0. X <= x \ y by Def11; hence x \ y in BCK-part X ; ::_thesis: verum end; theorem :: BCIALG_1:21 for X being BCI-algebra for x being Element of X for y being Element of BCK-part X holds x \ y <= x proof let X be BCI-algebra; ::_thesis: for x being Element of X for y being Element of BCK-part X holds x \ y <= x let x be Element of X; ::_thesis: for y being Element of BCK-part X holds x \ y <= x let y be Element of BCK-part X; ::_thesis: x \ y <= x y in { y1 where y1 is Element of X : 0. X <= y1 } ; then ex y1 being Element of X st ( y = y1 & 0. X <= y1 ) ; then y ` = 0. X by Def11; then (x \ x) \ y = 0. X by Def5; then (x \ y) \ x = 0. X by Th7; hence x \ y <= x by Def11; ::_thesis: verum end; theorem Th22: :: BCIALG_1:22 for X being BCI-algebra holds X is SubAlgebra of X proof let X be BCI-algebra; ::_thesis: X is SubAlgebra of X dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def_1; then ( 0. X = 0. X & the InternalDiff of X = the InternalDiff of X || the carrier of X ) by RELAT_1:68; hence X is SubAlgebra of X by Def10; ::_thesis: verum end; definition let X be BCI-algebra; let IT be SubAlgebra of X; attrIT is proper means :Def13: :: BCIALG_1:def 13 IT <> X; end; :: deftheorem Def13 defines proper BCIALG_1:def_13_:_ for X being BCI-algebra for IT being SubAlgebra of X holds ( IT is proper iff IT <> X ); registration let X be BCI-algebra; cluster non empty being_B being_C being_I being_BCI-4 non proper for SubAlgebra of X; existence not for b1 being SubAlgebra of X holds b1 is proper proof take X ; ::_thesis: ( X is SubAlgebra of X & not X is proper ) X is SubAlgebra of X by Th22; hence ( X is SubAlgebra of X & not X is proper ) by Def13; ::_thesis: verum end; end; definition let X be BCI-algebra; let IT be Element of X; attrIT is atom means :Def14: :: BCIALG_1:def 14 for z being Element of X st z \ IT = 0. X holds z = IT; end; :: deftheorem Def14 defines atom BCIALG_1:def_14_:_ for X being BCI-algebra for IT being Element of X holds ( IT is atom iff for z being Element of X st z \ IT = 0. X holds z = IT ); definition let X be BCI-algebra; func AtomSet X -> non empty Subset of X equals :: BCIALG_1:def 15 { x where x is Element of X : x is atom } ; coherence { x where x is Element of X : x is atom } is non empty Subset of X proof set Y = { x where x is Element of X : x is atom } ; A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_x_is_atom__}__holds_ y_in_the_carrier_of_X let y be set ; ::_thesis: ( y in { x where x is Element of X : x is atom } implies y in the carrier of X ) assume y in { x where x is Element of X : x is atom } ; ::_thesis: y in the carrier of X then ex x being Element of X st ( y = x & x is atom ) ; hence y in the carrier of X ; ::_thesis: verum end; for z being Element of X st z \ (0. X) = 0. X holds z = 0. X by Th2; then 0. X is atom by Def14; then 0. X in { x where x is Element of X : x is atom } ; hence { x where x is Element of X : x is atom } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines AtomSet BCIALG_1:def_15_:_ for X being BCI-algebra holds AtomSet X = { x where x is Element of X : x is atom } ; theorem Th23: :: BCIALG_1:23 for X being BCI-algebra holds 0. X in AtomSet X proof let X be BCI-algebra; ::_thesis: 0. X in AtomSet X for z being Element of X st z \ (0. X) = 0. X holds z = 0. X by Th2; then 0. X is atom by Def14; hence 0. X in AtomSet X ; ::_thesis: verum end; theorem Th24: :: BCIALG_1:24 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds z \ (z \ x) = x ) thus ( x in AtomSet X implies for z being Element of X holds z \ (z \ x) = x ) ::_thesis: ( ( for z being Element of X holds z \ (z \ x) = x ) implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: for z being Element of X holds z \ (z \ x) = x then A1: ex x1 being Element of X st ( x = x1 & x1 is atom ) ; let z be Element of X; ::_thesis: z \ (z \ x) = x (z \ (z \ x)) \ x = 0. X by Th1; hence z \ (z \ x) = x by A1, Def14; ::_thesis: verum end; assume A2: for z being Element of X holds z \ (z \ x) = x ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume z \ x = 0. X ; ::_thesis: z = x then z \ (0. X) = x by A2; hence z = x by Th2; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem :: BCIALG_1:25 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) thus ( x in AtomSet X implies for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) ::_thesis: ( ( for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ) implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u then A1: ex x1 being Element of X st ( x = x1 & x1 is atom ) ; let u, z be Element of X; ::_thesis: (z \ u) \ (z \ x) = x \ u (z \ (z \ x)) \ x = 0. X by Th1; then z \ (z \ x) = x by A1, Def14; hence (z \ u) \ (z \ x) = x \ u by Th7; ::_thesis: verum end; assume A2: for u, z being Element of X holds (z \ u) \ (z \ x) = x \ u ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume z \ x = 0. X ; ::_thesis: z = x then (z \ (0. X)) \ (0. X) = x \ (0. X) by A2; then (z \ (0. X)) \ (0. X) = x by Th2; then z \ (0. X) = x by Th2; hence z = x by Th2; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem :: BCIALG_1:26 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) thus ( x in AtomSet X implies for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) ::_thesis: ( ( for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ) implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) then A1: ex x1 being Element of X st ( x = x1 & x1 is atom ) ; let y, z be Element of X; ::_thesis: x \ (z \ y) <= y \ (z \ x) (z \ (z \ x)) \ x = 0. X by Th1; then (x \ (z \ y)) \ (y \ (z \ x)) = ((z \ (z \ x)) \ (z \ y)) \ (y \ (z \ x)) by A1, Def14; then (x \ (z \ y)) \ (y \ (z \ x)) = ((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x)) by Th7; then (x \ (z \ y)) \ (y \ (z \ x)) = (((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x))) \ (0. X) by Th2; then (x \ (z \ y)) \ (y \ (z \ x)) = (((z \ (z \ y)) \ (z \ x)) \ (y \ (z \ x))) \ ((z \ (z \ y)) \ y) by Th1; then (x \ (z \ y)) \ (y \ (z \ x)) = 0. X by Def3; hence x \ (z \ y) <= y \ (z \ x) by Def11; ::_thesis: verum end; assume A2: for y, z being Element of X holds x \ (z \ y) <= y \ (z \ x) ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume A3: z \ x = 0. X ; ::_thesis: z = x x \ (z \ (0. X)) <= (z \ x) ` by A2; then (x \ (z \ (0. X))) \ ((0. X) `) = 0. X by A3, Def11; then (x \ (z \ (0. X))) \ (0. X) = 0. X by Th2; then x \ (z \ (0. X)) = 0. X by Th2; then x \ z = 0. X by Th2; hence z = x by A3, Def7; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem :: BCIALG_1:27 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) thus ( x in AtomSet X implies for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) ::_thesis: ( ( for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ) implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) then A1: ex x1 being Element of X st ( x = x1 & x1 is atom ) ; let y, z, u be Element of X; ::_thesis: (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) (z \ (z \ x)) \ x = 0. X by Th1; then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ (z \ x)) \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) by A1, Def14; then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ u) \ (z \ x)) \ (z \ y)) \ ((y \ u) \ (z \ x)) by Th7; then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = (((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x)) by Th7 .= ((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) \ (0. X) by Th2 ; then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = ((((z \ u) \ (z \ y)) \ (z \ x)) \ ((y \ u) \ (z \ x))) \ (((z \ u) \ (z \ y)) \ (y \ u)) by Th1; then ((x \ u) \ (z \ y)) \ ((y \ u) \ (z \ x)) = 0. X by Def3; hence (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) by Def11; ::_thesis: verum end; assume A2: for y, z, u being Element of X holds (x \ u) \ (z \ y) <= (y \ u) \ (z \ x) ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume A3: z \ x = 0. X ; ::_thesis: z = x (x \ (0. X)) \ (z \ (0. X)) <= ((0. X) `) \ (z \ x) by A2; then ((x \ (0. X)) \ (z \ (0. X))) \ (((0. X) `) \ (0. X)) = 0. X by A3, Def11; then ((x \ (0. X)) \ (z \ (0. X))) \ ((0. X) `) = 0. X by Th2; then ((x \ (0. X)) \ (z \ (0. X))) \ (0. X) = 0. X by Th2; then (x \ (0. X)) \ (z \ (0. X)) = 0. X by Th2; then (x \ (0. X)) \ z = 0. X by Th2; then x \ z = 0. X by Th2; hence z = x by A3, Def7; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem Th28: :: BCIALG_1:28 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds (z `) \ (x `) = x \ z ) thus ( x in AtomSet X implies for z being Element of X holds (z `) \ (x `) = x \ z ) ::_thesis: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: for z being Element of X holds (z `) \ (x `) = x \ z then A1: ex x1 being Element of X st ( x = x1 & x1 is atom ) ; let z be Element of X; ::_thesis: (z `) \ (x `) = x \ z (z \ (z \ x)) \ x = 0. X by Th1; then z \ (z \ x) = x by A1, Def14; then x \ z = (z \ z) \ (z \ x) by Th7; then x \ z = (z \ x) ` by Def5; hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum end; assume A2: for z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume A3: z \ x = 0. X ; ::_thesis: z = x then (z \ x) ` = 0. X by Def5; then (z `) \ (x `) = 0. X by Th9; then x \ z = 0. X by A2; hence z = x by A3, Def7; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem Th29: :: BCIALG_1:29 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff (x `) ` = x ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff (x `) ` = x ) let x be Element of X; ::_thesis: ( x in AtomSet X iff (x `) ` = x ) thus ( x in AtomSet X implies (x `) ` = x ) ::_thesis: ( (x `) ` = x implies x in AtomSet X ) proof assume x in AtomSet X ; ::_thesis: (x `) ` = x then ((0. X) `) \ (x `) = x \ (0. X) by Th28; then ((0. X) `) \ (x `) = x by Th2; hence (x `) ` = x by Def5; ::_thesis: verum end; assume A1: (x `) ` = x ; ::_thesis: x in AtomSet X now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume A2: z \ x = 0. X ; ::_thesis: z = x then ((z \ x) \ (x `)) \ (z \ (0. X)) = x \ z by A1, Th2; then 0. X = x \ z by Def3; hence z = x by A2, Def7; ::_thesis: verum end; then x is atom by Def14; hence x in AtomSet X ; ::_thesis: verum end; theorem Th30: :: BCIALG_1:30 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) A1: ( ( for z being Element of X holds (z `) \ (x `) = x \ z ) implies for z being Element of X holds (z \ x) ` = x \ z ) proof assume A2: for z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: for z being Element of X holds (z \ x) ` = x \ z let z be Element of X; ::_thesis: (z \ x) ` = x \ z (z `) \ (x `) = x \ z by A2; hence (z \ x) ` = x \ z by Th9; ::_thesis: verum end; ( ( for z being Element of X holds (z \ x) ` = x \ z ) implies for z being Element of X holds (z `) \ (x `) = x \ z ) proof assume A3: for z being Element of X holds (z \ x) ` = x \ z ; ::_thesis: for z being Element of X holds (z `) \ (x `) = x \ z let z be Element of X; ::_thesis: (z `) \ (x `) = x \ z (z \ x) ` = x \ z by A3; hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum end; hence ( x in AtomSet X iff for z being Element of X holds (z \ x) ` = x \ z ) by A1, Th28; ::_thesis: verum end; theorem Th31: :: BCIALG_1:31 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for z being Element of X holds ((x \ z) `) ` = x \ z ) thus ( x in AtomSet X implies for z being Element of X holds ((x \ z) `) ` = x \ z ) ::_thesis: ( ( for z being Element of X holds ((x \ z) `) ` = x \ z ) implies x in AtomSet X ) proof assume A1: x in AtomSet X ; ::_thesis: for z being Element of X holds ((x \ z) `) ` = x \ z let z be Element of X; ::_thesis: ((x \ z) `) ` = x \ z A2: (z \ (z \ x)) \ x = 0. X by Th1; ex x1 being Element of X st ( x = x1 & x1 is atom ) by A1; then z \ (z \ x) = x by A2, Def14; then ((x \ z) `) ` = (((z \ z) \ (z \ x)) `) ` by Th7; then ((x \ z) `) ` = (((z \ x) `) `) ` by Def5; then ((x \ z) `) ` = (z \ x) ` by Th8; hence ((x \ z) `) ` = x \ z by A1, Th30; ::_thesis: verum end; assume for z being Element of X holds ((x \ z) `) ` = x \ z ; ::_thesis: x in AtomSet X then ((x \ (0. X)) `) ` = x \ (0. X) ; then (x `) ` = x \ (0. X) by Th2; then (x `) ` = x by Th2; hence x in AtomSet X by Th29; ::_thesis: verum end; theorem :: BCIALG_1:32 for X being BCI-algebra for x being Element of X holds ( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) proof let X be BCI-algebra; ::_thesis: for x being Element of X holds ( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) let x be Element of X; ::_thesis: ( x in AtomSet X iff for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) thus ( x in AtomSet X implies for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) ::_thesis: ( ( for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ) implies x in AtomSet X ) proof assume A1: x in AtomSet X ; ::_thesis: for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u let z, u be Element of X; ::_thesis: z \ (z \ (x \ u)) = x \ u x \ u = ((x \ u) `) ` by A1, Th31 .= ((z \ z) \ (x \ u)) ` by Def5 .= ((z \ (x \ u)) \ z) ` by Th7 .= ((z \ (x \ u)) `) \ (z `) by Th9 ; then A2: (x \ u) \ (z \ (z \ (x \ u))) = 0. X by Th1; (z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1; hence z \ (z \ (x \ u)) = x \ u by A2, Def7; ::_thesis: verum end; assume for z, u being Element of X holds z \ (z \ (x \ u)) = x \ u ; ::_thesis: x in AtomSet X then for u being Element of X holds ((x \ u) `) ` = x \ u ; hence x in AtomSet X by Th31; ::_thesis: verum end; theorem Th33: :: BCIALG_1:33 for X being BCI-algebra for a being Element of AtomSet X for x being Element of X holds a \ x in AtomSet X proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for x being Element of X holds a \ x in AtomSet X let a be Element of AtomSet X; ::_thesis: for x being Element of X holds a \ x in AtomSet X let x be Element of X; ::_thesis: a \ x in AtomSet X ((a \ x) `) ` = a \ x by Th31; hence a \ x in AtomSet X by Th29; ::_thesis: verum end; definition let X be BCI-algebra; let a, b be Element of AtomSet X; :: original: \ redefine funca \ b -> Element of AtomSet X; coherence a \ b is Element of AtomSet X by Th33; end; theorem Th34: :: BCIALG_1:34 for X being BCI-algebra for x being Element of X holds x ` in AtomSet X proof let X be BCI-algebra; ::_thesis: for x being Element of X holds x ` in AtomSet X let x be Element of X; ::_thesis: x ` in AtomSet X 0. X in AtomSet X by Th23; hence x ` in AtomSet X by Th33; ::_thesis: verum end; theorem Th35: :: BCIALG_1:35 for X being BCI-algebra for x being Element of X ex a being Element of AtomSet X st a <= x proof let X be BCI-algebra; ::_thesis: for x being Element of X ex a being Element of AtomSet X st a <= x let x be Element of X; ::_thesis: ex a being Element of AtomSet X st a <= x take a = (x `) ` ; ::_thesis: ( a is Element of AtomSet X & a <= x ) a \ x = 0. X by Th1; hence ( a is Element of AtomSet X & a <= x ) by Def11, Th34; ::_thesis: verum end; definition let X be BCI-algebra; attrX is generated_by_atom means :Def16: :: BCIALG_1:def 16 for x being Element of X ex a being Element of AtomSet X st a <= x; end; :: deftheorem Def16 defines generated_by_atom BCIALG_1:def_16_:_ for X being BCI-algebra holds ( X is generated_by_atom iff for x being Element of X ex a being Element of AtomSet X st a <= x ); definition let X be BCI-algebra; let a be Element of AtomSet X; func BranchV a -> non empty Subset of X equals :: BCIALG_1:def 17 { x where x is Element of X : a <= x } ; coherence { x where x is Element of X : a <= x } is non empty Subset of X proof set Y = { x where x is Element of X : a <= x } ; A1: now__::_thesis:_for_y_being_set_st_y_in__{__x_where_x_is_Element_of_X_:_a_<=_x__}__holds_ y_in_the_carrier_of_X let y be set ; ::_thesis: ( y in { x where x is Element of X : a <= x } implies y in the carrier of X ) assume y in { x where x is Element of X : a <= x } ; ::_thesis: y in the carrier of X then ex x being Element of X st ( y = x & a <= x ) ; hence y in the carrier of X ; ::_thesis: verum end; a \ a = 0. X by Def5; then a <= a by Def11; then a in { x where x is Element of X : a <= x } ; hence { x where x is Element of X : a <= x } is non empty Subset of X by A1, TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem defines BranchV BCIALG_1:def_17_:_ for X being BCI-algebra for a being Element of AtomSet X holds BranchV a = { x where x is Element of X : a <= x } ; theorem :: BCIALG_1:36 for X being BCI-algebra holds X is generated_by_atom proof let X be BCI-algebra; ::_thesis: X is generated_by_atom for x being Element of X ex a being Element of AtomSet X st a <= x by Th35; hence X is generated_by_atom by Def16; ::_thesis: verum end; theorem :: BCIALG_1:37 for X being BCI-algebra for a, b being Element of AtomSet X for x being Element of BranchV b holds a \ x = a \ b proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X for x being Element of BranchV b holds a \ x = a \ b let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV b holds a \ x = a \ b let x be Element of BranchV b; ::_thesis: a \ x = a \ b a \ b in { x1 where x1 is Element of X : x1 is atom } ; then A1: ex x1 being Element of X st ( a \ b = x1 & x1 is atom ) ; x in { yy where yy is Element of X : b <= yy } ; then A2: ex yy being Element of X st ( x = yy & b <= yy ) ; (a \ x) \ (a \ b) = (a \ (a \ b)) \ x by Th7; then (a \ x) \ (a \ b) = b \ x by Th24; then (a \ x) \ (a \ b) = 0. X by A2, Def11; hence a \ x = a \ b by A1, Def14; ::_thesis: verum end; theorem Th38: :: BCIALG_1:38 for X being BCI-algebra for a being Element of AtomSet X for x being Element of BCK-part X holds a \ x = a proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for x being Element of BCK-part X holds a \ x = a let a be Element of AtomSet X; ::_thesis: for x being Element of BCK-part X holds a \ x = a let x be Element of BCK-part X; ::_thesis: a \ x = a a \ (0. X) in { x1 where x1 is Element of X : x1 is atom } by Th33; then A1: ex x1 being Element of X st ( a \ (0. X) = x1 & x1 is atom ) ; (a \ x) \ (a \ (0. X)) = (a \ (a \ (0. X))) \ x by Th7; then (a \ x) \ (a \ (0. X)) = (a \ a) \ x by Th2; then A2: (a \ x) \ (a \ (0. X)) = x ` by Def5; x in { x2 where x2 is Element of X : 0. X <= x2 } ; then ex x2 being Element of X st ( x = x2 & 0. X <= x2 ) ; then (a \ x) \ (a \ (0. X)) = 0. X by A2, Def11; then a \ x = a \ (0. X) by A1, Def14; hence a \ x = a by Th2; ::_thesis: verum end; Lm2: for X being BCI-algebra for a being Element of AtomSet X for x being Element of BranchV a holds a \ x = 0. X proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for x being Element of BranchV a holds a \ x = 0. X let a be Element of AtomSet X; ::_thesis: for x being Element of BranchV a holds a \ x = 0. X let x be Element of BranchV a; ::_thesis: a \ x = 0. X x in { x1 where x1 is Element of X : a <= x1 } ; then ex x1 being Element of X st ( x = x1 & a <= x1 ) ; hence a \ x = 0. X by Def11; ::_thesis: verum end; theorem Th39: :: BCIALG_1:39 for X being BCI-algebra for a, b being Element of AtomSet X for x being Element of BranchV a for y being Element of BranchV b holds x \ y in BranchV (a \ b) proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X for x being Element of BranchV a for y being Element of BranchV b holds x \ y in BranchV (a \ b) let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV a for y being Element of BranchV b holds x \ y in BranchV (a \ b) let x be Element of BranchV a; ::_thesis: for y being Element of BranchV b holds x \ y in BranchV (a \ b) let y be Element of BranchV b; ::_thesis: x \ y in BranchV (a \ b) (a \ b) \ (x \ y) = (((a \ b) `) `) \ (x \ y) by Th29; then (a \ b) \ (x \ y) = ((x \ y) `) \ ((a \ b) `) by Th7; then (a \ b) \ (x \ y) = ((x `) \ (y `)) \ ((a \ b) `) by Th9; then (a \ b) \ (x \ y) = ((x `) \ ((a \ b) `)) \ (y `) by Th7; then (a \ b) \ (x \ y) = ((((a \ b) `) `) \ x) \ (y `) by Th7; then (a \ b) \ (x \ y) = ((a \ b) \ x) \ (y `) by Th29; then (a \ b) \ (x \ y) = ((a \ x) \ b) \ (y `) by Th7; then (a \ b) \ (x \ y) = (b `) \ (y `) by Lm2; then (a \ b) \ (x \ y) = (b \ y) ` by Th9; then (a \ b) \ (x \ y) = (0. X) ` by Lm2; then (a \ b) \ (x \ y) = 0. X by Def5; then a \ b <= x \ y by Def11; hence x \ y in BranchV (a \ b) ; ::_thesis: verum end; theorem :: BCIALG_1:40 for X being BCI-algebra for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ y in BCK-part X proof let X be BCI-algebra; ::_thesis: for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ y in BCK-part X let a be Element of AtomSet X; ::_thesis: for x, y being Element of BranchV a holds x \ y in BCK-part X let x, y be Element of BranchV a; ::_thesis: x \ y in BCK-part X set b = a \ a; ( a \ a = 0. X & x \ y in BranchV (a \ a) ) by Def5, Th39; hence x \ y in BCK-part X ; ::_thesis: verum end; theorem :: BCIALG_1:41 for X being BCI-algebra for a, b being Element of AtomSet X for x being Element of BranchV a for y being Element of BranchV b st a <> b holds not x \ y in BCK-part X proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X for x being Element of BranchV a for y being Element of BranchV b st a <> b holds not x \ y in BCK-part X let a, b be Element of AtomSet X; ::_thesis: for x being Element of BranchV a for y being Element of BranchV b st a <> b holds not x \ y in BCK-part X let x be Element of BranchV a; ::_thesis: for y being Element of BranchV b st a <> b holds not x \ y in BCK-part X let y be Element of BranchV b; ::_thesis: ( a <> b implies not x \ y in BCK-part X ) assume A1: a <> b ; ::_thesis: not x \ y in BCK-part X x \ y in BranchV (a \ b) by Th39; then ex xy being Element of X st ( x \ y = xy & a \ b <= xy ) ; then (a \ b) \ (x \ y) = 0. X by Def11; then (a \ (x \ y)) \ b = 0. X by Th7; then (a \ (x \ y)) \ ((a \ (x \ y)) \ b) = a \ (x \ y) by Th2; then A2: b = a \ (x \ y) by Th24; assume x \ y in BCK-part X ; ::_thesis: contradiction hence contradiction by A1, A2, Th38; ::_thesis: verum end; theorem :: BCIALG_1:42 for X being BCI-algebra for a, b being Element of AtomSet X st a <> b holds (BranchV a) /\ (BranchV b) = {} proof let X be BCI-algebra; ::_thesis: for a, b being Element of AtomSet X st a <> b holds (BranchV a) /\ (BranchV b) = {} let a, b be Element of AtomSet X; ::_thesis: ( a <> b implies (BranchV a) /\ (BranchV b) = {} ) assume A1: a <> b ; ::_thesis: (BranchV a) /\ (BranchV b) = {} assume (BranchV a) /\ (BranchV b) <> {} ; ::_thesis: contradiction then consider c being set such that A2: c in (BranchV a) /\ (BranchV b) by XBOOLE_0:def_1; reconsider z2 = c as Element of BranchV b by A2, XBOOLE_0:def_4; reconsider z1 = c as Element of BranchV a by A2, XBOOLE_0:def_4; z1 \ z2 in BranchV (a \ b) by Th39; then 0. X in { x3 where x3 is Element of X : a \ b <= x3 } by Def5; then ex x3 being Element of X st ( 0. X = x3 & a \ b <= x3 ) ; then (a \ b) \ (0. X) = 0. X by Def11; then A3: a \ b = 0. X by Th2; b in { xx where xx is Element of X : xx is atom } ; then ex xx being Element of X st ( b = xx & xx is atom ) ; hence contradiction by A1, A3, Def14; ::_thesis: verum end; definition let X be BCI-algebra; mode Ideal of X -> non empty Subset of X means :Def18: :: BCIALG_1:def 18 ( 0. X in it & ( for x, y being Element of X st x \ y in it & y in it holds x in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y being Element of X st x \ y in b1 & y in b1 holds x in b1 ) ) proof take X1 = {(0. X)}; ::_thesis: ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds x in X1 ) ) A1: for x, y being Element of X st x \ y in X1 & y in X1 holds x in X1 proof let x, y be Element of X; ::_thesis: ( x \ y in X1 & y in X1 implies x in X1 ) assume ( x \ y in X1 & y in X1 ) ; ::_thesis: x in X1 then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1; then x = 0. X by Th2; hence x in X1 by TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_for_xx_being_set_st_xx_in_X1_holds_ xx_in_the_carrier_of_X let xx be set ; ::_thesis: ( xx in X1 implies xx in the carrier of X ) assume xx in X1 ; ::_thesis: xx in the carrier of X then xx = 0. X by TARSKI:def_1; hence xx in the carrier of X ; ::_thesis: verum end; hence ( X1 is non empty Subset of X & 0. X in X1 & ( for x, y being Element of X st x \ y in X1 & y in X1 holds x in X1 ) ) by A1, TARSKI:def_1, TARSKI:def_3; ::_thesis: verum end; end; :: deftheorem Def18 defines Ideal BCIALG_1:def_18_:_ for X being BCI-algebra for b2 being non empty Subset of X holds ( b2 is Ideal of X iff ( 0. X in b2 & ( for x, y being Element of X st x \ y in b2 & y in b2 holds x in b2 ) ) ); definition let X be BCI-algebra; let IT be Ideal of X; attrIT is closed means :Def19: :: BCIALG_1:def 19 for x being Element of IT holds x ` in IT; end; :: deftheorem Def19 defines closed BCIALG_1:def_19_:_ for X being BCI-algebra for IT being Ideal of X holds ( IT is closed iff for x being Element of IT holds x ` in IT ); Lm3: for X being BCI-algebra holds {(0. X)} is Ideal of X proof let X be BCI-algebra; ::_thesis: {(0. X)} is Ideal of X set X1 = {(0. X)}; now__::_thesis:_for_xx_being_set_st_xx_in_{(0._X)}_holds_ xx_in_the_carrier_of_X let xx be set ; ::_thesis: ( xx in {(0. X)} implies xx in the carrier of X ) assume xx in {(0. X)} ; ::_thesis: xx in the carrier of X then xx = 0. X by TARSKI:def_1; hence xx in the carrier of X ; ::_thesis: verum end; then A1: {(0. X)} is Subset of X by TARSKI:def_3; A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds x in {(0. X)} proof set X1 = {(0. X)}; let x, y be Element of X; ::_thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} ) assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; ::_thesis: x in {(0. X)} then ( x \ y = 0. X & y = 0. X ) by TARSKI:def_1; then x = 0. X by Th2; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; 0. X in {(0. X)} by TARSKI:def_1; hence {(0. X)} is Ideal of X by A1, A2, Def18; ::_thesis: verum end; Lm4: for X being BCI-algebra for X1 being Ideal of X st X1 = {(0. X)} holds for x being Element of X1 holds x ` in {(0. X)} proof let X be BCI-algebra; ::_thesis: for X1 being Ideal of X st X1 = {(0. X)} holds for x being Element of X1 holds x ` in {(0. X)} let X1 be Ideal of X; ::_thesis: ( X1 = {(0. X)} implies for x being Element of X1 holds x ` in {(0. X)} ) assume A1: X1 = {(0. X)} ; ::_thesis: for x being Element of X1 holds x ` in {(0. X)} let x be Element of X1; ::_thesis: x ` in {(0. X)} x = 0. X by A1, TARSKI:def_1; then x ` = 0. X by Def5; hence x ` in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; registration let X be BCI-algebra; cluster non empty closed for Ideal of X; existence ex b1 being Ideal of X st b1 is closed proof set X1 = {(0. X)}; reconsider X1 = {(0. X)} as Ideal of X by Lm3; take X1 ; ::_thesis: X1 is closed for x being Element of X1 holds x ` in X1 by Lm4; hence X1 is closed by Def19; ::_thesis: verum end; end; theorem :: BCIALG_1:43 for X being BCI-algebra holds {(0. X)} is closed Ideal of X proof let X be BCI-algebra; ::_thesis: {(0. X)} is closed Ideal of X set X1 = {(0. X)}; reconsider X1 = {(0. X)} as Ideal of X by Lm3; for x being Element of X1 holds x ` in X1 by Lm4; hence {(0. X)} is closed Ideal of X by Def19; ::_thesis: verum end; theorem :: BCIALG_1:44 for X being BCI-algebra holds the carrier of X is closed Ideal of X proof let X be BCI-algebra; ::_thesis: the carrier of X is closed Ideal of X A1: ( ( for x being Element of X holds x ` in the carrier of X ) & ( for x, y being Element of X st x \ y in the carrier of X & y in the carrier of X holds x in the carrier of X ) ) ; ( the carrier of X is non empty Subset of X & 0. X in the carrier of X ) by ZFMISC_1:def_1; hence the carrier of X is closed Ideal of X by A1, Def18, Def19; ::_thesis: verum end; theorem :: BCIALG_1:45 for X being BCI-algebra holds BCK-part X is closed Ideal of X proof let X be BCI-algebra; ::_thesis: BCK-part X is closed Ideal of X set X1 = BCK-part X; A1: for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds x in BCK-part X proof let x, y be Element of X; ::_thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X ) assume that A2: x \ y in BCK-part X and A3: y in BCK-part X ; ::_thesis: x in BCK-part X ex x1 being Element of X st ( x \ y = x1 & 0. X <= x1 ) by A2; then (x \ y) ` = 0. X by Def11; then A4: (x `) \ (y `) = 0. X by Th9; ex x2 being Element of X st ( y = x2 & 0. X <= x2 ) by A3; then (x `) \ (0. X) = 0. X by A4, Def11; then x ` = 0. X by Th2; then 0. X <= x by Def11; hence x in BCK-part X ; ::_thesis: verum end; 0. X in BCK-part X by Th19; then reconsider X1 = BCK-part X as Ideal of X by A1, Def18; now__::_thesis:_for_x_being_Element_of_X1_holds_x_`_in_X1 let x be Element of X1; ::_thesis: x ` in X1 x in X1 ; then ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) ; then x ` = 0. X by Def11; then (x `) ` = 0. X by Def5; then 0. X <= x ` by Def11; hence x ` in X1 ; ::_thesis: verum end; hence BCK-part X is closed Ideal of X by Def19; ::_thesis: verum end; Lm5: for X being BCI-algebra for IT being non empty Subset of X st IT is Ideal of X holds for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT proof let X be BCI-algebra; ::_thesis: for IT being non empty Subset of X st IT is Ideal of X holds for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT let IT be non empty Subset of X; ::_thesis: ( IT is Ideal of X implies for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT ) assume A1: IT is Ideal of X ; ::_thesis: for x, y being Element of IT holds { z where z is Element of X : z \ x <= y } c= IT let x, y be Element of IT; ::_thesis: { z where z is Element of X : z \ x <= y } c= IT A2: 0. X in IT by A1, Def18; for ss being set st ss in { z where z is Element of X : z \ x <= y } holds ss in IT proof let ss be set ; ::_thesis: ( ss in { z where z is Element of X : z \ x <= y } implies ss in IT ) assume ss in { z where z is Element of X : z \ x <= y } ; ::_thesis: ss in IT then A3: ex z being Element of X st ( ss = z & z \ x <= y ) ; then reconsider ss = ss as Element of X ; (ss \ x) \ y in IT by A2, A3, Def11; then ss \ x in IT by A1, Def18; hence ss in IT by A1, Def18; ::_thesis: verum end; hence { z where z is Element of X : z \ x <= y } c= IT by TARSKI:def_3; ::_thesis: verum end; theorem :: BCIALG_1:46 for X being BCI-algebra for IT being non empty Subset of X st IT is Ideal of X holds for x, y being Element of X st x in IT & y <= x holds y in IT proof let X be BCI-algebra; ::_thesis: for IT being non empty Subset of X st IT is Ideal of X holds for x, y being Element of X st x in IT & y <= x holds y in IT let IT be non empty Subset of X; ::_thesis: ( IT is Ideal of X implies for x, y being Element of X st x in IT & y <= x holds y in IT ) assume A1: IT is Ideal of X ; ::_thesis: for x, y being Element of X st x in IT & y <= x holds y in IT let x, y be Element of X; ::_thesis: ( x in IT & y <= x implies y in IT ) assume that A2: x in IT and A3: y <= x ; ::_thesis: y in IT y \ (0. X) <= x by A3, Th2; then A4: y in { z where z is Element of X : z \ (0. X) <= x } ; 0. X is Element of IT by A1, Def18; then { z where z is Element of X : z \ (0. X) <= x } c= IT by A1, A2, Lm5; hence y in IT by A4; ::_thesis: verum end; begin definition let IT be BCI-algebra; attrIT is associative means :Def20: :: BCIALG_1:def 20 for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z); attrIT is quasi-associative means :Def21: :: BCIALG_1:def 21 for x being Element of IT holds (x `) ` = x ` ; attrIT is positive-implicative means :Def22: :: BCIALG_1:def 22 for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))); attrIT is weakly-positive-implicative means :Def23: :: BCIALG_1:def 23 for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z); attrIT is implicative means :Def24: :: BCIALG_1:def 24 for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x); attrIT is weakly-implicative means :: BCIALG_1:def 25 for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x; attrIT is p-Semisimple means :Def26: :: BCIALG_1:def 26 for x, y being Element of IT holds x \ (x \ y) = y; attrIT is alternative means :Def27: :: BCIALG_1:def 27 for x, y being Element of IT holds ( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ); end; :: deftheorem Def20 defines associative BCIALG_1:def_20_:_ for IT being BCI-algebra holds ( IT is associative iff for x, y, z being Element of IT holds (x \ y) \ z = x \ (y \ z) ); :: deftheorem Def21 defines quasi-associative BCIALG_1:def_21_:_ for IT being BCI-algebra holds ( IT is quasi-associative iff for x being Element of IT holds (x `) ` = x ` ); :: deftheorem Def22 defines positive-implicative BCIALG_1:def_22_:_ for IT being BCI-algebra holds ( IT is positive-implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ); :: deftheorem Def23 defines weakly-positive-implicative BCIALG_1:def_23_:_ for IT being BCI-algebra holds ( IT is weakly-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) ); :: deftheorem Def24 defines implicative BCIALG_1:def_24_:_ for IT being BCI-algebra holds ( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ); :: deftheorem defines weakly-implicative BCIALG_1:def_25_:_ for IT being BCI-algebra holds ( IT is weakly-implicative iff for x, y being Element of IT holds (x \ (y \ x)) \ ((y \ x) `) = x ); :: deftheorem Def26 defines p-Semisimple BCIALG_1:def_26_:_ for IT being BCI-algebra holds ( IT is p-Semisimple iff for x, y being Element of IT holds x \ (x \ y) = y ); :: deftheorem Def27 defines alternative BCIALG_1:def_27_:_ for IT being BCI-algebra holds ( IT is alternative iff for x, y being Element of IT holds ( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) ); registration cluster BCI-EXAMPLE -> associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple ; coherence ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) proof set IT = BCI-EXAMPLE ; A1: BCI-EXAMPLE is positive-implicative proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_22 ::_thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) thus (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by STRUCT_0:def_10; ::_thesis: verum end; A2: BCI-EXAMPLE is p-Semisimple proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_26 ::_thesis: x \ (x \ y) = y x \ (x \ y) = {} by CARD_1:49, TARSKI:def_1; hence x \ (x \ y) = y by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A3: BCI-EXAMPLE is weakly-implicative proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_25 ::_thesis: (x \ (y \ x)) \ ((y \ x) `) = x (x \ (y \ x)) \ ((y \ x) `) = {} by CARD_1:49, TARSKI:def_1; hence (x \ (y \ x)) \ ((y \ x) `) = x by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A4: BCI-EXAMPLE is associative proof let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_20 ::_thesis: (x \ y) \ z = x \ (y \ z) (x \ y) \ z = {} by CARD_1:49, TARSKI:def_1; hence (x \ y) \ z = x \ (y \ z) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A5: BCI-EXAMPLE is weakly-positive-implicative proof let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_23 ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z) thus (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by STRUCT_0:def_10; ::_thesis: verum end; BCI-EXAMPLE is implicative proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def_24 ::_thesis: (x \ (x \ y)) \ (y \ x) = y \ (y \ x) thus (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum end; hence ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) by A1, A2, A4, A3, A5; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 associative positive-implicative weakly-positive-implicative implicative weakly-implicative p-Semisimple for BCIStr_0 ; existence ex b1 being BCI-algebra st ( b1 is implicative & b1 is positive-implicative & b1 is p-Semisimple & b1 is associative & b1 is weakly-implicative & b1 is weakly-positive-implicative ) proof take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) thus ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) ; ::_thesis: verum end; end; Lm6: for X being BCI-algebra st ( for x, y being Element of X holds y \ x = x \ y ) holds X is associative proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative ) assume A1: for x, y being Element of X holds y \ x = x \ y ; ::_thesis: X is associative let x, y, z be Element of X; :: according to BCIALG_1:def_20 ::_thesis: (x \ y) \ z = x \ (y \ z) x \ (y \ z) = (y \ z) \ x by A1 .= (y \ x) \ z by Th7 ; hence (x \ y) \ z = x \ (y \ z) by A1; ::_thesis: verum end; Lm7: for X being BCI-algebra st ( for x being Element of X holds x ` = x ) holds for x, y being Element of X holds x \ y = y \ x proof let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds x ` = x ) implies for x, y being Element of X holds x \ y = y \ x ) assume A1: for x being Element of X holds x ` = x ; ::_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 A2: (y \ x) \ (x \ y) = ((y `) \ x) \ (x \ y) by A1 .= ((y `) \ (x `)) \ (x \ y) by A1 .= 0. X by Th1 ; (x \ y) \ (y \ x) = ((x `) \ y) \ (y \ x) by A1 .= ((x `) \ (y `)) \ (y \ x) by A1 .= 0. X by Th1 ; hence x \ y = y \ x by A2, Def7; ::_thesis: verum end; theorem Th47: :: BCIALG_1:47 for X being BCI-algebra holds ( X is associative iff for x being Element of X holds x ` = x ) proof let X be BCI-algebra; ::_thesis: ( X is associative iff for x being Element of X holds x ` = x ) thus ( X is associative implies for x being Element of X holds x ` = x ) ::_thesis: ( ( for x being Element of X holds x ` = x ) implies X is associative ) proof assume A1: X is associative ; ::_thesis: for x being Element of X holds x ` = x let x be Element of X; ::_thesis: x ` = x A2: x \ (x `) = (x \ (0. X)) \ x by A1, Def20 .= x \ x by Th2 .= 0. X by Def5 ; (x `) \ x = (x \ x) ` by A1, Def20 .= (0. X) ` by Def5 .= 0. X by Def5 ; hence x ` = x by A2, Def7; ::_thesis: verum end; assume for x being Element of X holds x ` = x ; ::_thesis: X is associative then for x, y being Element of X holds x \ y = y \ x by Lm7; hence X is associative by Lm6; ::_thesis: verum end; theorem Th48: :: BCIALG_1:48 for X being BCI-algebra holds ( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative ) proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative ) thus ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative ) by Lm6; ::_thesis: ( X is associative implies for x, y being Element of X holds y \ x = x \ y ) assume X is associative ; ::_thesis: for x, y being Element of X holds y \ x = x \ y then for x being Element of X holds x ` = x by Th47; hence for x, y being Element of X holds y \ x = x \ y by Lm7; ::_thesis: verum end; theorem Th49: :: BCIALG_1:49 for X being non empty BCIStr_0 holds ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) proof assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) let x, y, z be Element of X; ::_thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (y \ x)) \ (z \ x) by A1, Def20; then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (y \ x) by A1, Th7; then (z \ y) \ ((y \ x) \ (z \ x)) = ((z \ y) \ (z \ x)) \ (x \ y) by A1, Th48; then A2: (z \ y) \ ((y \ x) \ (z \ x)) = 0. X by A1, Th1; ((y \ x) \ (z \ x)) \ (z \ y) = ((y \ x) \ (z \ x)) \ (y \ z) by A1, Th48; then ((y \ x) \ (z \ x)) \ (z \ y) = 0. X by A1, Def3; hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A1, A2, Def7, Th2; ::_thesis: verum end; thus ( ( for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) ::_thesis: verum proof assume A3: for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) ; ::_thesis: X is associative BCI-algebra A4: for x, y being Element of X holds y \ x = x \ y proof let x, y be Element of X; ::_thesis: y \ x = x \ y (y \ (0. X)) \ (x \ (0. X)) = x \ y by A3; then y \ (x \ (0. X)) = x \ y by A3; hence y \ x = x \ y by A3; ::_thesis: verum end; A5: for a being Element of X holds a \ a = 0. X proof let a be Element of X; ::_thesis: a \ a = 0. X (a `) \ (a `) = (0. X) ` by A3; then (a \ (0. X)) \ (a `) = (0. X) ` by A4; then (a \ (0. X)) \ (a \ (0. X)) = (0. X) ` by A4; then a \ a = (0. X) ` by A3; hence a \ a = 0. X by A3; ::_thesis: verum end; A6: for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) proof let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) ((x \ y) \ (x \ z)) \ (z \ y) = ((y \ x) \ (x \ z)) \ (z \ y) by A4 .= ((y \ x) \ (z \ x)) \ (z \ y) by A4 .= (z \ y) \ (z \ y) by A3 ; hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A5; ::_thesis: (x \ (x \ y)) \ y = 0. X (x `) \ (y \ x) = y \ (0. X) by A3; then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4; then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4; then x \ (x \ y) = y \ (0. X) by A3; then (x \ (x \ y)) \ y = y \ y by A3; hence (x \ (x \ y)) \ y = 0. X by A5; ::_thesis: verum end; 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 A7: x \ y = 0. X and y \ x = 0. X ; ::_thesis: x = y (x `) \ (y \ x) = y \ (0. X) by A3; then (x \ (0. X)) \ (y \ x) = y \ (0. X) by A4; then (x \ (0. X)) \ (x \ y) = y \ (0. X) by A4; then x \ (x \ y) = y \ (0. X) by A3; then y = x \ (x \ y) by A3 .= x by A3, A7 ; hence x = y ; ::_thesis: verum end; then A8: X is being_BCI-4 by Def7; X is being_I by A5, Def5; then reconsider Y = X as BCI-algebra by A6, A8, Th1; Y is associative by A4, Th48; hence X is associative BCI-algebra ; ::_thesis: verum end; end; theorem Th50: :: BCIALG_1:50 for X being non empty BCIStr_0 holds ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) ) implies X is associative BCI-algebra ) proof assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x ) (y \ x) \ (z \ x) = z \ y by A1, Th49; then A2: (x \ y) \ (z \ x) = z \ y by A1, Th48; x \ (0. X) = x by A1, Th49; hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A1, A2, Th48; ::_thesis: verum end; assume A3: for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) ; ::_thesis: X is associative BCI-algebra for x, y, z being Element of X holds ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) proof A4: for x, y being Element of X holds y \ x = x \ y proof let x, y be Element of X; ::_thesis: y \ x = x \ y (y `) \ (x `) = x \ y by A3; then y \ (x `) = x \ y by A3; hence y \ x = x \ y by A3; ::_thesis: verum end; let x, y, z be Element of X; ::_thesis: ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) A5: x ` = x by A3; (x \ y) \ (x \ z) = z \ y by A3; then (y \ x) \ (x \ z) = z \ y by A4; hence ( (y \ x) \ (z \ x) = z \ y & x \ (0. X) = x ) by A4, A5; ::_thesis: verum end; hence X is associative BCI-algebra by Th49; ::_thesis: verum end; theorem :: BCIALG_1:51 for X being non empty BCIStr_0 holds ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is associative BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) thus ( X is associative BCI-algebra implies for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) ::_thesis: ( ( for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ) implies X is associative BCI-algebra ) proof assume A1: X is associative BCI-algebra ; ::_thesis: for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) (y \ x) \ (z \ x) = z \ y by A1, Th49; then (x \ y) \ (z \ x) = z \ y by A1, Th48; then (x \ y) \ (x \ z) = z \ y by A1, Th48; hence ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A1, Th48, Th49; ::_thesis: verum end; assume A2: for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) ; ::_thesis: X is associative BCI-algebra for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x ` = x ) proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ (x \ z) = z \ y & x ` = x ) A3: for x, y being Element of X holds y \ x = x \ y proof let x, y be Element of X; ::_thesis: y \ x = x \ y (x \ (0. X)) \ (x \ (0. X)) = (0. X) ` by A2; then x \ (x \ (0. X)) = (0. X) ` by A2; then x \ x = (0. X) ` by A2; then A4: x \ x = 0. X by A2; (x \ y) \ (x \ x) = y \ x by A2; hence y \ x = x \ y by A2, A4; ::_thesis: verum end; ( (x \ y) \ (x \ z) = y \ z & x \ (0. X) = x ) by A2; hence ( (x \ y) \ (x \ z) = z \ y & x ` = x ) by A3; ::_thesis: verum end; hence X is associative BCI-algebra by Th50; ::_thesis: verum end; begin theorem :: BCIALG_1:52 for X being BCI-algebra holds ( X is p-Semisimple iff for x being Element of X holds x is atom ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X holds x is atom ) thus ( X is p-Semisimple implies for x being Element of X holds x is atom ) ::_thesis: ( ( for x being Element of X holds x is atom ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x being Element of X holds x is atom let x be Element of X; ::_thesis: x is atom now__::_thesis:_for_z_being_Element_of_X_st_z_\_x_=_0._X_holds_ z_=_x let z be Element of X; ::_thesis: ( z \ x = 0. X implies z = x ) assume z \ x = 0. X ; ::_thesis: z = x then z \ (0. X) = x by A1, Def26; hence z = x by Th2; ::_thesis: verum end; hence x is atom by Def14; ::_thesis: verum end; assume A2: for x being Element of X holds x is atom ; ::_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 ( y is atom & (x \ (x \ y)) \ y = 0. X ) by A2, Th1; hence x \ (x \ y) = y by Def14; ::_thesis: verum end; hence X is p-Semisimple by Def26; ::_thesis: verum end; theorem :: BCIALG_1:53 for X being BCI-algebra st X is p-Semisimple holds BCK-part X = {(0. X)} proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies BCK-part X = {(0. X)} ) assume A1: X is p-Semisimple ; ::_thesis: BCK-part X = {(0. X)} thus BCK-part X c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= BCK-part X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in BCK-part X or x in {(0. X)} ) assume A2: x in BCK-part X ; ::_thesis: x in {(0. X)} then A3: ex x1 being Element of X st ( x = x1 & 0. X <= x1 ) ; reconsider x = x as Element of X by A2; (x `) ` = x by A1, Def26; then (0. X) ` = x by A3, Def11; then x = 0. X by Def5; hence x in {(0. X)} by TARSKI:def_1; ::_thesis: verum end; thus {(0. X)} c= BCK-part X ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. X)} or x in BCK-part X ) assume A4: x in {(0. X)} ; ::_thesis: x in BCK-part X then reconsider x = x as Element of X by TARSKI:def_1; x = 0. X by A4, TARSKI:def_1; then x ` = 0. X by Def5; then 0. X <= x by Def11; hence x in BCK-part X ; ::_thesis: verum end; end; Lm8: for X being BCI-algebra holds ( ( for x being Element of X holds (x `) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x ) proof let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds (x `) ` = x ) iff for x, y being Element of X holds y \ (y \ x) = x ) thus ( ( for x being Element of X holds (x `) ` = x ) implies for x, y being Element of X holds y \ (y \ x) = x ) ::_thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x ) proof assume A1: for x being Element of X holds (x `) ` = x ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x let x, y be Element of X; ::_thesis: y \ (y \ x) = x A2: (y \ (y \ x)) \ x = 0. X by Th1; x \ (y \ (y \ x)) = ((x \ (y \ (y \ x))) `) ` by A1 .= ((x `) \ ((y \ (y \ x)) `)) ` by Th9 .= (0. X) \ (((x `) \ ((y \ (y \ x)) `)) \ (0. X)) by Th2 .= (0. X) \ ((((0. X) \ x) \ ((y \ (y \ x)) `)) \ ((y \ (y \ x)) \ x)) by Th1 .= (0. X) \ (0. X) by Th1 .= 0. X by Def5 ; hence y \ (y \ x) = x by A2, Def7; ::_thesis: verum end; thus ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x being Element of X holds (x `) ` = x ) ; ::_thesis: verum end; Lm9: for X being BCI-algebra holds ( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x ) iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) thus ( ( for x, y being Element of X holds y \ (y \ x) = x ) implies for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) ::_thesis: ( ( for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) implies for x, y being Element of X holds y \ (y \ x) = x ) proof assume A1: for x, y being Element of X holds y \ (y \ x) = x ; ::_thesis: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y let x, y, z be Element of X; ::_thesis: (z \ y) \ (z \ x) = x \ y (z \ y) \ (z \ x) = (z \ (z \ x)) \ y by Th7; hence (z \ y) \ (z \ x) = x \ y by A1; ::_thesis: verum end; assume A2: for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x let x, y be Element of X; ::_thesis: y \ (y \ x) = x (y \ (0. X)) \ (y \ x) = x \ (0. X) by A2; then y \ (y \ x) = x \ (0. X) by Th2; hence y \ (y \ x) = x by Th2; ::_thesis: verum end; theorem Th54: :: BCIALG_1:54 for X being BCI-algebra holds ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) ( ( for x being Element of X holds (x `) ` = x ) implies X is p-Semisimple ) proof assume A1: for x being Element of X holds (x `) ` = x ; ::_thesis: X is p-Semisimple now__::_thesis:_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y let x, y be Element of X; ::_thesis: x \ (x \ y) = y A2: (x \ (x \ y)) \ y = 0. X by Th1; y \ (x \ (x \ y)) = ((y \ (x \ (x \ y))) `) ` by A1 .= ((y `) \ ((x \ (x \ y)) `)) ` by Th9 .= (0. X) \ ((((0. X) \ y) \ ((x \ (x \ y)) `)) \ (0. X)) by Th2 .= (0. X) \ ((((0. X) \ y) \ ((x \ (x \ y)) `)) \ ((x \ (x \ y)) \ y)) by Th1 .= (0. X) \ (0. X) by Th1 .= 0. X by Def5 ; hence x \ (x \ y) = y by A2, Def7; ::_thesis: verum end; hence X is p-Semisimple by Def26; ::_thesis: verum end; hence ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) by Def26; ::_thesis: verum end; theorem Th55: :: BCIALG_1:55 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) by Th54; hence ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) by Lm8; ::_thesis: verum end; theorem Th56: :: BCIALG_1:56 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) ( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) by Th55; hence ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) by Lm9; ::_thesis: verum end; theorem Th57: :: BCIALG_1:57 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) thus ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) ::_thesis: ( ( for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) let x, y, z be Element of X; ::_thesis: x \ (z \ y) = y \ (z \ x) y \ (z \ x) = (z \ (z \ y)) \ (z \ x) by A1, Def26; then A2: (y \ (z \ x)) \ (x \ (z \ y)) = 0. X by Th1; x \ (z \ y) = (z \ (z \ x)) \ (z \ y) by A1, Def26; then (x \ (z \ y)) \ (y \ (z \ x)) = 0. X by Th1; hence x \ (z \ y) = y \ (z \ x) by A2, Def7; ::_thesis: verum end; assume A3: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ; ::_thesis: X is p-Semisimple for x being Element of X holds (x `) ` = x proof let x be Element of X; ::_thesis: (x `) ` = x (x `) ` = x \ ((0. X) `) by A3 .= x \ (0. X) by Def5 ; hence (x `) ` = x by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; Lm10: for X being BCI-algebra st X is p-Semisimple holds for x, y, z, u being Element of X holds ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z, u being Element of X holds ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) ) assume A1: X is p-Semisimple ; ::_thesis: for x, y, z, u being Element of X holds ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) let x, y, z, u be Element of X; ::_thesis: ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) A2: (x \ u) \ (z \ y) = (x \ (z \ y)) \ u by Th7 .= (y \ (z \ x)) \ u by A1, Th57 ; (x \ u) \ (z \ y) = y \ (z \ (x \ u)) by A1, Th57 .= y \ (u \ (x \ z)) by A1, Th57 .= (x \ z) \ (u \ y) by A1, Th57 ; hence ( (x \ u) \ (z \ y) = (y \ u) \ (z \ x) & (x \ u) \ (z \ y) = (x \ z) \ (u \ y) ) by A2, Th7; ::_thesis: verum end; Lm11: for X being BCI-algebra st X is p-Semisimple holds for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y ) assume A1: X is p-Semisimple ; ::_thesis: for x, y being Element of X holds (y `) \ ((0. X) \ x) = x \ y let x, y be Element of X; ::_thesis: (y `) \ ((0. X) \ x) = x \ y (y `) \ ((0. X) \ x) = (x \ y) \ ((0. X) \ (0. X)) by A1, Lm10 .= (x \ y) \ (0. X) by Def5 ; hence (y `) \ ((0. X) \ x) = x \ y by Th2; ::_thesis: verum end; Lm12: for X being BCI-algebra st X is p-Semisimple holds for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z let x, y, z be Element of X; ::_thesis: (x \ y) \ (z \ y) = x \ z (x \ y) \ (z \ y) = (x \ z) \ (y \ y) by A1, Lm10 .= (x \ z) \ (0. X) by Def5 ; hence (x \ y) \ (z \ y) = x \ z by Th2; ::_thesis: verum end; Lm13: for X being BCI-algebra st X is p-Semisimple holds for x, y, z being Element of X st x \ y = x \ z holds y = z proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X st x \ y = x \ z holds y = z ) assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X st x \ y = x \ z holds y = z let x, y, z be Element of X; ::_thesis: ( x \ y = x \ z implies y = z ) assume A2: x \ y = x \ z ; ::_thesis: y = z (x \ z) \ (x \ y) = (y \ z) \ (x \ x) by A1, Lm10; then (x \ z) \ (x \ y) = (y \ z) \ (0. X) by Def5; then (x \ z) \ (x \ y) = y \ z by Th2; then A3: 0. X = y \ z by A2, Def5; (x \ y) \ (x \ z) = (z \ y) \ (x \ x) by A1, Lm10; then (x \ y) \ (x \ z) = (z \ y) \ (0. X) by Def5; then (x \ y) \ (x \ z) = z \ y by Th2; then 0. X = z \ y by A2, Def5; hence y = z by A3, Def7; ::_thesis: verum end; Lm14: for X being BCI-algebra st X is p-Semisimple holds for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) let x, y, z be Element of X; ::_thesis: x \ (y \ z) = (z \ y) \ (x `) x \ (y \ z) = z \ (y \ x) by A1, Th57 .= (z \ (0. X)) \ (y \ x) by Th2 ; hence x \ (y \ z) = (z \ y) \ (x `) by A1, Lm10; ::_thesis: verum end; Lm15: for X being BCI-algebra st X is p-Semisimple holds for x, y, z being Element of X st y \ x = z \ x holds y = z proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds y = z ) assume A1: X is p-Semisimple ; ::_thesis: for x, y, z being Element of X st y \ x = z \ x holds y = z let x, y, z be Element of X; ::_thesis: ( y \ x = z \ x implies y = z ) assume A2: y \ x = z \ x ; ::_thesis: y = z A3: z \ y = (z \ x) \ (y \ x) by A1, Lm12 .= 0. X by A2, Def5 ; y \ z = (y \ x) \ (z \ x) by A1, Lm12 .= 0. X by A2, Def5 ; hence y = z by A3, Def7; ::_thesis: verum end; theorem :: BCIALG_1:58 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) thus ( X is p-Semisimple implies for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) by Lm10; ::_thesis: ( ( for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) implies X is p-Semisimple ) thus ( ( for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ) implies X is p-Semisimple ) ::_thesis: verum proof assume A1: for x, y, z, u being Element of X holds (x \ u) \ (z \ y) = (y \ u) \ (z \ x) ; ::_thesis: X is p-Semisimple for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) proof let x, y, z be Element of X; ::_thesis: x \ (z \ y) = y \ (z \ x) (x \ (0. X)) \ (z \ y) = (y \ (0. X)) \ (z \ x) by A1; then x \ (z \ y) = (y \ (0. X)) \ (z \ x) by Th2; hence x \ (z \ y) = y \ (z \ x) by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th57; ::_thesis: verum end; end; theorem Th59: :: BCIALG_1:59 for X being BCI-algebra holds ( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z ) thus ( X is p-Semisimple implies for x, z being Element of X holds (z `) \ (x `) = x \ z ) by Lm11; ::_thesis: ( ( for x, z being Element of X holds (z `) \ (x `) = x \ z ) implies X is p-Semisimple ) assume A1: for x, z being Element of X holds (z `) \ (x `) = x \ z ; ::_thesis: X is p-Semisimple for x being Element of X holds (x `) ` = x proof let x be Element of X; ::_thesis: (x `) ` = x ((0. X) `) \ (x `) = x \ (0. X) by A1; then (x `) ` = x \ (0. X) by Th2; hence (x `) ` = x by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; theorem :: BCIALG_1:60 for X being BCI-algebra holds ( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, z being Element of X holds ((x \ z) `) ` = x \ z ) thus ( X is p-Semisimple implies for x, z being Element of X holds ((x \ z) `) ` = x \ z ) ::_thesis: ( ( for x, z being Element of X holds ((x \ z) `) ` = x \ z ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x, z being Element of X holds ((x \ z) `) ` = x \ z let x, z be Element of X; ::_thesis: ((x \ z) `) ` = x \ z ((x \ z) `) ` = ((x `) \ (z `)) ` by Th9 .= (z \ x) ` by A1, Th59 .= (z `) \ (x `) by Th9 ; hence ((x \ z) `) ` = x \ z by A1, Th59; ::_thesis: verum end; assume A2: for x, z being Element of X holds ((x \ z) `) ` = x \ z ; ::_thesis: X is p-Semisimple now__::_thesis:_for_x_being_Element_of_X_holds_(x_`)_`_=_x let x be Element of X; ::_thesis: (x `) ` = x ((x \ (0. X)) `) ` = x \ (0. X) by A2; then (x `) ` = x \ (0. X) by Th2; hence (x `) ` = x by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; theorem :: BCIALG_1:61 for X being BCI-algebra holds ( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) thus ( X is p-Semisimple implies for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) ::_thesis: ( ( for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u let x, u, z be Element of X; ::_thesis: z \ (z \ (x \ u)) = x \ u (z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1 .= (x \ u) \ (x \ u) by Def5 ; hence z \ (z \ (x \ u)) = x \ u by A1, Lm15; ::_thesis: verum end; assume A2: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ; ::_thesis: X is p-Semisimple now__::_thesis:_for_x_being_Element_of_X_holds_(x_`)_`_=_x let x be Element of X; ::_thesis: (x `) ` = x ((x \ (0. X)) `) ` = x \ (0. X) by A2; then ((x \ (0. X)) `) ` = x by Th2; hence (x `) ` = x by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; theorem Th62: :: BCIALG_1:62 for X being BCI-algebra holds ( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds x = 0. X ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds x = 0. X ) thus ( X is p-Semisimple implies for x being Element of X st x ` = 0. X holds x = 0. X ) ::_thesis: ( ( for x being Element of X st x ` = 0. X holds x = 0. X ) implies X is p-Semisimple ) proof assume A1: X is p-Semisimple ; ::_thesis: for x being Element of X st x ` = 0. X holds x = 0. X let x be Element of X; ::_thesis: ( x ` = 0. X implies x = 0. X ) assume x ` = 0. X ; ::_thesis: x = 0. X then (x `) ` = 0. X by Def5; hence x = 0. X by A1, Def26; ::_thesis: verum end; assume A2: for x being Element of X st x ` = 0. X holds x = 0. X ; ::_thesis: X is p-Semisimple for x being Element of X holds (x `) ` = x proof let x be Element of X; ::_thesis: (x `) ` = x (x \ ((x `) `)) ` = (x `) \ (((x `) `) `) by Th9 .= (x `) \ (x `) by Th8 .= 0. X by Def5 ; then A3: x \ ((x `) `) = 0. X by A2; ((x `) `) \ x = 0. X by Th1; hence (x `) ` = x by A3, Def7; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; theorem Th63: :: BCIALG_1:63 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y being Element of X holds x \ (y `) = y \ (x `) ) thus ( X is p-Semisimple implies for x, y being Element of X holds x \ (y `) = y \ (x `) ) by Th57; ::_thesis: ( ( for x, y being Element of X holds x \ (y `) = y \ (x `) ) implies X is p-Semisimple ) assume A1: for x, y being Element of X holds x \ (y `) = y \ (x `) ; ::_thesis: X is p-Semisimple now__::_thesis:_for_x_being_Element_of_X_holds_x_=_(x_`)_` let x be Element of X; ::_thesis: x = (x `) ` x \ ((0. X) `) = (x `) ` by A1; then x \ (0. X) = (x `) ` by Th2; hence x = (x `) ` by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th54; ::_thesis: verum end; theorem :: BCIALG_1:64 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) thus ( X is p-Semisimple implies for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) by Lm10; ::_thesis: ( ( for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ) implies X is p-Semisimple ) assume A1: for x, y, z, u being Element of X holds (x \ y) \ (z \ u) = (x \ z) \ (y \ u) ; ::_thesis: X is p-Semisimple for x, z being Element of X holds (z `) \ (x `) = x \ z proof let x, z be Element of X; ::_thesis: (z `) \ (x `) = x \ z (z \ x) ` = (x \ x) \ (z \ x) by Def5; then (z \ x) ` = (x \ z) \ (x \ x) by A1; then (z \ x) ` = (x \ z) \ (0. X) by Def5; then (z \ x) ` = x \ z by Th2; hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum end; hence X is p-Semisimple by Th59; ::_thesis: verum end; theorem :: BCIALG_1:65 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) thus ( X is p-Semisimple implies for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) by Lm12; ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ) implies X is p-Semisimple ) assume A1: for x, y, z being Element of X holds (x \ y) \ (z \ y) = x \ z ; ::_thesis: X is p-Semisimple for x, z being Element of X holds (z `) \ (x `) = x \ z proof let x, z be Element of X; ::_thesis: (z `) \ (x `) = x \ z (z \ x) ` = (x \ x) \ (z \ x) by Def5; then (z \ x) ` = x \ z by A1; hence (z `) \ (x `) = x \ z by Th9; ::_thesis: verum end; hence X is p-Semisimple by Th59; ::_thesis: verum end; theorem :: BCIALG_1:66 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) thus ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) by Lm14; ::_thesis: ( ( for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ) implies X is p-Semisimple ) assume A1: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x `) ; ::_thesis: X is p-Semisimple for x, y being Element of X holds x \ (y `) = y \ (x `) proof let x, y be Element of X; ::_thesis: x \ (y `) = y \ (x `) x \ (y `) = (y \ (0. X)) \ (x `) by A1; hence x \ (y `) = y \ (x `) by Th2; ::_thesis: verum end; hence X is p-Semisimple by Th63; ::_thesis: verum end; theorem :: BCIALG_1:67 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds y = z ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X st y \ x = z \ x holds y = z ) thus ( X is p-Semisimple implies for x, y, z being Element of X st y \ x = z \ x holds y = z ) by Lm15; ::_thesis: ( ( for x, y, z being Element of X st y \ x = z \ x holds y = z ) implies X is p-Semisimple ) assume A1: for x, y, z being Element of X st y \ x = z \ x holds y = z ; ::_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 = 0. X by Th1; then (x \ (x \ y)) \ y = y \ y by Def5; hence x \ (x \ y) = y by A1; ::_thesis: verum end; hence X is p-Semisimple by Def26; ::_thesis: verum end; theorem :: BCIALG_1:68 for X being BCI-algebra holds ( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds y = z ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple iff for x, y, z being Element of X st x \ y = x \ z holds y = z ) thus ( X is p-Semisimple implies for x, y, z being Element of X st x \ y = x \ z holds y = z ) by Lm13; ::_thesis: ( ( for x, y, z being Element of X st x \ y = x \ z holds y = z ) implies X is p-Semisimple ) assume A1: for x, y, z being Element of X st x \ y = x \ z holds y = z ; ::_thesis: X is p-Semisimple for x being Element of X st x ` = 0. X holds x = 0. X proof let x be Element of X; ::_thesis: ( x ` = 0. X implies x = 0. X ) assume x ` = 0. X ; ::_thesis: x = 0. X then x ` = (0. X) ` by Def5; hence x = 0. X by A1; ::_thesis: verum end; hence X is p-Semisimple by Th62; ::_thesis: verum end; theorem :: BCIALG_1:69 for X being non empty BCIStr_0 holds ( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) thus ( X is p-Semisimple BCI-algebra implies for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) by Th2, Th56; ::_thesis: ( ( for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra ) assume A1: for x, y, z being Element of X holds ( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) ; ::_thesis: X is p-Semisimple BCI-algebra A2: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_(_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y_)_) let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) ) ((x \ y) \ (x \ z)) \ (z \ y) = (z \ y) \ (z \ y) by A1 .= ((z \ y) \ (0. X)) \ (z \ y) by A1 .= ((z \ y) \ (0. X)) \ ((z \ y) \ (0. X)) by A1 .= (0. X) ` by A1 ; hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) ) (x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1 .= (y \ (0. X)) \ y by A1 .= (y \ (0. X)) \ (y \ (0. X)) by A1 .= (0. X) ` by A1 ; hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y thus for x, y being Element of X holds x \ (x \ y) = y ::_thesis: verum proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A1; then x \ (x \ y) = y \ (0. X) by A1; hence x \ (x \ y) = y by A1; ::_thesis: verum end; end; now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_ x_=_y let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume that A3: x \ y = 0. X and y \ x = 0. X ; ::_thesis: x = y x = x \ (0. X) by A1 .= (x \ (0. X)) \ (x \ y) by A1, A3 .= y \ (0. X) by A1 ; hence x = y by A1; ::_thesis: verum end; then A4: X is being_BCI-4 by Def7; now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X let x be Element of X; ::_thesis: x \ x = 0. X x \ x = (x \ (0. X)) \ x by A1 .= (x \ (0. X)) \ (x \ (0. X)) by A1 .= (0. X) ` by A1 ; hence x \ x = 0. X by A1; ::_thesis: verum end; then X is being_I by Def5; hence X is p-Semisimple BCI-algebra by A4, A2, Def26, Th1; ::_thesis: verum end; theorem :: BCIALG_1:70 for X being non empty BCIStr_0 holds ( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds ( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is p-Semisimple BCI-algebra iff ( X is being_I & ( for x, y, z being Element of X holds ( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) thus ( X is p-Semisimple BCI-algebra implies ( X is being_I & ( for x, y, z being Element of X holds ( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) ) ) by Th2, Th57; ::_thesis: ( X is being_I & ( for x, y, z being Element of X holds ( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ) implies X is p-Semisimple BCI-algebra ) assume that A1: X is being_I and A2: for x, y, z being Element of X holds ( x \ (y \ z) = z \ (y \ x) & x \ (0. X) = x ) ; ::_thesis: X is p-Semisimple BCI-algebra A3: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_x_\_x_=_0._X_&_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_&_(_for_x,_y_being_Element_of_X_holds_x_\_(x_\_y)_=_y_)_) let x, y, z be Element of X; ::_thesis: ( x \ x = 0. X & ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) ) thus x \ x = 0. X by A1, Def5; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) ) ((x \ y) \ (x \ z)) \ (z \ y) = (z \ (x \ (x \ y))) \ (z \ y) by A2 .= (z \ (y \ (x \ x))) \ (z \ y) by A2 .= (z \ (y \ (0. X))) \ (z \ y) by A1, Def5 .= (z \ y) \ (z \ y) by A2 ; hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1, Def5; ::_thesis: ( (x \ (x \ y)) \ y = 0. X & ( for x, y being Element of X holds x \ (x \ y) = y ) ) (x \ (x \ y)) \ y = (y \ (x \ x)) \ y by A2 .= (y \ (0. X)) \ y by A1, Def5 .= y \ y by A2 ; hence (x \ (x \ y)) \ y = 0. X by A1, Def5; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y thus for x, y being Element of X holds x \ (x \ y) = y ::_thesis: verum proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y x \ (x \ y) = y \ (x \ x) by A2; then x \ (x \ y) = y \ (0. X) by A1, Def5; hence x \ (x \ y) = y by A2; ::_thesis: verum end; end; now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_ x_=_y 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 y \ x = 0. X ; ::_thesis: x = y x = x \ (0. X) by A2 .= y \ (x \ x) by A2, A4 .= y \ (0. X) by A1, Def5 ; hence x = y by A2; ::_thesis: verum end; then X is being_BCI-4 by Def7; hence X is p-Semisimple BCI-algebra by A1, A3, Def26, Th1; ::_thesis: verum end; begin Lm16: for X being BCI-algebra st ( for x being Element of X holds x ` <= x ) holds for x, y being Element of X holds (x \ y) ` = (y \ x) ` proof let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds x ` <= x ) implies for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) assume A1: for x being Element of X holds x ` <= x ; ::_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 Th8 .= (((y `) \ (x `)) `) ` by Th9 .= (((y `) `) \ ((x `) `)) ` by Th9 .= ((((x `) `) `) \ (y `)) ` by Th7 .= ((x `) \ (y `)) ` by Th8 .= ((x \ y) `) ` by Th9 ; then (y \ x) ` <= (x \ y) ` by A1; then A2: ((y \ x) `) \ ((x \ y) `) = 0. X by Def11; (x \ y) ` = (((x \ y) `) `) ` by Th8 .= (((x `) \ (y `)) `) ` by Th9 .= (((x `) `) \ ((y `) `)) ` by Th9 .= ((((y `) `) `) \ (x `)) ` by Th7 .= ((y `) \ (x `)) ` by Th8 .= ((y \ x) `) ` by Th9 ; then (x \ y) ` <= (y \ x) ` by A1; then ((x \ y) `) \ ((y \ x) `) = 0. X by Def11; hence (x \ y) ` = (y \ x) ` by A2, Def7; ::_thesis: verum end; Lm17: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) holds for x, y being Element of X holds (x `) \ y = (x \ y) ` proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) implies for x, y being Element of X holds (x `) \ y = (x \ y) ` ) assume A1: for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; ::_thesis: for x, y being Element of X holds (x `) \ y = (x \ y) ` let x, y be Element of X; ::_thesis: (x `) \ y = (x \ y) ` thus (x \ y) ` = (x `) \ (y `) by Th9 .= ((y `) `) \ x by Th7 .= ((y \ (0. X)) `) \ x by A1 .= (y `) \ x by Th2 .= (x `) \ y by Th7 ; ::_thesis: verum end; Lm18: for X being BCI-algebra st ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) holds for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) assume A1: for x, y being Element of X holds (x `) \ y = (x \ y) ` ; ::_thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X let x, y be Element of X; ::_thesis: (x \ y) \ (y \ x) in BCK-part X ((x \ y) \ (y \ x)) ` = ((x \ y) `) \ (y \ x) by A1 .= ((x `) \ (y `)) \ (y \ x) by Th9 .= (((y `) `) \ x) \ (y \ x) by Th7 .= (((y `) \ x) `) \ (y \ x) by A1 .= (((y \ x) `) `) \ (y \ x) by A1 .= 0. X by Th1 ; then 0. X <= (x \ y) \ (y \ x) by Def11; hence (x \ y) \ (y \ x) in BCK-part X ; ::_thesis: verum end; Lm19: for X being BCI-algebra st ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) holds X is quasi-associative proof let X be BCI-algebra; ::_thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative ) assume A1: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ; ::_thesis: X is quasi-associative for x being Element of X holds (x `) ` = x ` proof let x be Element of X; ::_thesis: (x `) ` = x ` x \ (x `) = (x \ (0. X)) \ (x `) by Th2; then x \ (x `) in { x2 where x2 is Element of X : 0. X <= x2 } by A1; then ex x2 being Element of X st ( x \ (x `) = x2 & 0. X <= x2 ) ; then (x \ (x `)) ` = 0. X by Def11; then A2: (x `) \ ((x `) `) = 0. X by Th9; (x `) \ x = (x `) \ (x \ (0. X)) by Th2; then (x `) \ x in { x1 where x1 is Element of X : 0. X <= x1 } by A1; then ex x1 being Element of X st ( (x `) \ x = x1 & 0. X <= x1 ) ; then ((x `) \ x) ` = 0. X by Def11; then ((x `) `) \ (x `) = 0. X by Th9; hence (x `) ` = x ` by A2, Def7; ::_thesis: verum end; hence X is quasi-associative by Def21; ::_thesis: verum end; Lm20: for X being BCI-algebra holds ( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) proof let X be BCI-algebra; ::_thesis: ( ( for x being Element of X holds x ` <= x ) iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) thus ( ( for x being Element of X holds x ` <= x ) implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies for x being Element of X holds x ` <= x ) proof assume A1: for x being Element of X holds x ` <= x ; ::_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 \ z) = 0. X by Th1; then A2: ((x \ (x \ (y \ z))) \ y) \ ((y \ z) \ y) = 0. X by Th4; ((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7 .= ((x \ (x \ (y \ z))) \ y) \ z by Th7 ; then (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ z) \ y) \ z) = 0. X by A2, Th4; then A3: (((x \ y) \ z) \ (x \ (y \ z))) \ (((y \ y) \ z) \ z) = 0. X by Th7; z ` <= z by A1; then (z `) \ z = 0. X by Def11; then (((x \ y) \ z) \ (x \ (y \ z))) \ (0. X) = 0. X by A3, Def5; then ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by Th2; hence (x \ y) \ z <= x \ (y \ z) by Def11; ::_thesis: verum end; assume A4: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ; ::_thesis: for x being Element of X holds x ` <= x let x be Element of X; ::_thesis: x ` <= x ((0. X) `) \ x <= (x `) ` by A4; then x ` <= (x `) ` by Def5; then (x `) \ ((x `) `) = 0. X by Def11; then (((x `) `) `) \ x = 0. X by Th7; then (x `) \ x = 0. X by Th8; hence x ` <= x by Def11; ::_thesis: verum end; theorem Th71: :: BCIALG_1:71 for X being BCI-algebra holds ( X is quasi-associative iff for x being Element of X holds x ` <= x ) proof let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x being Element of X holds x ` <= x ) thus ( X is quasi-associative implies for x being Element of X holds x ` <= x ) ::_thesis: ( ( for x being Element of X holds x ` <= x ) implies X is quasi-associative ) proof assume A1: X is quasi-associative ; ::_thesis: for x being Element of X holds x ` <= x let x be Element of X; ::_thesis: x ` <= x ((x `) `) \ x = 0. X by Th1; then (x `) \ x = 0. X by A1, Def21; hence x ` <= x by Def11; ::_thesis: verum end; assume for x being Element of X holds x ` <= x ; ::_thesis: X is quasi-associative then for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Lm16; then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17; then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18; hence X is quasi-associative by Lm19; ::_thesis: verum end; theorem Th72: :: BCIALG_1:72 for X being BCI-algebra holds ( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) proof let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) ::_thesis: ( ( for x, y being Element of X holds (x \ y) ` = (y \ x) ` ) implies X is quasi-associative ) proof assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x \ y) ` = (y \ x) ` then for x being Element of X holds x ` <= x by Th71; hence for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Lm16; ::_thesis: verum end; assume for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; ::_thesis: X is quasi-associative then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17; then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18; hence X is quasi-associative by Lm19; ::_thesis: verum end; theorem Th73: :: BCIALG_1:73 for X being BCI-algebra holds ( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` ) proof let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` ) thus ( X is quasi-associative implies for x, y being Element of X holds (x `) \ y = (x \ y) ` ) ::_thesis: ( ( for x, y being Element of X holds (x `) \ y = (x \ y) ` ) implies X is quasi-associative ) proof assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x `) \ y = (x \ y) ` then for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Th72; hence for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm17; ::_thesis: verum end; assume for x, y being Element of X holds (x `) \ y = (x \ y) ` ; ::_thesis: X is quasi-associative then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18; hence X is quasi-associative by Lm19; ::_thesis: verum end; theorem :: BCIALG_1:74 for X being BCI-algebra holds ( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) proof let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) thus ( X is quasi-associative implies for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) ::_thesis: ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative ) proof assume X is quasi-associative ; ::_thesis: for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Th73; hence for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm18; ::_thesis: verum end; thus ( ( for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X ) implies X is quasi-associative ) by Lm19; ::_thesis: verum end; theorem :: BCIALG_1:75 for X being BCI-algebra holds ( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) proof let X be BCI-algebra; ::_thesis: ( X is quasi-associative iff for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) thus ( X is quasi-associative implies for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ) implies X is quasi-associative ) proof assume X is quasi-associative ; ::_thesis: for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) then for x being Element of X holds x ` <= x by Th71; hence for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) by Lm20; ::_thesis: verum end; assume for x, y, z being Element of X holds (x \ y) \ z <= x \ (y \ z) ; ::_thesis: X is quasi-associative then for x being Element of X holds x ` <= x by Lm20; hence X is quasi-associative by Th71; ::_thesis: verum end; begin theorem Th76: :: BCIALG_1:76 for X being BCI-algebra for x, y being Element of X st X is alternative holds ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative holds ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) let x, y be Element of X; ::_thesis: ( X is alternative implies ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) ) assume A1: X is alternative ; ::_thesis: ( x ` = x & x \ (x \ y) = y & (x \ y) \ y = x ) then x \ (x \ x) = (x \ x) \ x by Def27; then x \ (0. X) = (x \ x) \ x by Def5; then x \ (0. X) = x ` by Def5; hence x ` = x by Th2; ::_thesis: ( x \ (x \ y) = y & (x \ y) \ y = x ) y \ (y \ y) = (y \ y) \ y by A1, Def27; then y \ (0. X) = (y \ y) \ y by Def5; then y \ (0. X) = y ` by Def5; then A2: y = y ` by Th2; x \ (x \ y) = (x \ x) \ y by A1, Def27; hence x \ (x \ y) = y by A2, Def5; ::_thesis: (x \ y) \ y = x (x \ y) \ y = x \ (y \ y) by A1, Def27; then (x \ y) \ y = x \ (0. X) by Def5; hence (x \ y) \ y = x by Th2; ::_thesis: verum end; theorem :: BCIALG_1:77 for X being BCI-algebra for x, a, b being Element of X st X is alternative & x \ a = x \ b holds a = b proof let X be BCI-algebra; ::_thesis: for x, a, b being Element of X st X is alternative & x \ a = x \ b holds a = b let x, a, b be Element of X; ::_thesis: ( X is alternative & x \ a = x \ b implies a = b ) assume that A1: X is alternative and A2: x \ a = x \ b ; ::_thesis: a = b (x \ x) \ a = x \ (x \ b) by A1, A2, Def27; then (x \ x) \ a = (x \ x) \ b by A1, Def27; then a ` = (x \ x) \ b by Def5; then a ` = b ` by Def5; then a = b ` by A1, Th76; hence a = b by A1, Th76; ::_thesis: verum end; theorem :: BCIALG_1:78 for X being BCI-algebra for a, x, b being Element of X st X is alternative & a \ x = b \ x holds a = b proof let X be BCI-algebra; ::_thesis: for a, x, b being Element of X st X is alternative & a \ x = b \ x holds a = b let a, x, b be Element of X; ::_thesis: ( X is alternative & a \ x = b \ x implies a = b ) assume that A1: X is alternative and A2: a \ x = b \ x ; ::_thesis: a = b a \ (x \ x) = (b \ x) \ x by A1, A2, Def27; then a \ (x \ x) = b \ (x \ x) by A1, Def27; then a \ (0. X) = b \ (x \ x) by Def5; then a \ (0. X) = b \ (0. X) by Def5; then a = b \ (0. X) by Th2; hence a = b by Th2; ::_thesis: verum end; theorem :: BCIALG_1:79 for X being BCI-algebra for x, y being Element of X st X is alternative & x \ y = 0. X holds x = y proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative & x \ y = 0. X holds x = y let x, y be Element of X; ::_thesis: ( X is alternative & x \ y = 0. X implies x = y ) assume that A1: X is alternative and A2: x \ y = 0. X ; ::_thesis: x = y x \ (x \ y) = x by A2, Th2; then (x \ x) \ y = x by A1, Def27; then y ` = x by Def5; hence x = y by A1, Th76; ::_thesis: verum end; theorem :: BCIALG_1:80 for X being BCI-algebra for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds ( a = x \ b & b = x \ a ) proof let X be BCI-algebra; ::_thesis: for x, a, b being Element of X st X is alternative & (x \ a) \ b = 0. X holds ( a = x \ b & b = x \ a ) let x, a, b be Element of X; ::_thesis: ( X is alternative & (x \ a) \ b = 0. X implies ( a = x \ b & b = x \ a ) ) assume that A1: X is alternative and A2: (x \ a) \ b = 0. X ; ::_thesis: ( a = x \ b & b = x \ a ) (x \ a) \ (b \ b) = b ` by A1, A2, Def27; then (x \ a) \ (0. X) = b ` by Def5; then x \ a = b ` by Th2; then x \ (x \ a) = x \ b by A1, Th76; then (x \ x) \ a = x \ b by A1, Def27; then a ` = x \ b by Def5; then a = x \ b by A1, Th76; hence ( a = x \ b & b = x \ a ) by A1, Th76; ::_thesis: verum end; Lm21: for X being BCI-algebra holds ( X is alternative iff X is associative ) proof let X be BCI-algebra; ::_thesis: ( X is alternative iff X is associative ) thus ( X is alternative implies X is associative ) ::_thesis: ( X is associative implies X is alternative ) proof assume A1: X is alternative ; ::_thesis: X is associative 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) (((x \ y) \ y) \ ((x \ y) \ z)) \ (z \ y) = 0. X by Th1; then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ y) \ (y \ z)) = 0. X by Th4; then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ (y \ z)) \ y) = 0. X by Th7; then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ y) = 0. X by A1, Th76; then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ (y `)) = 0. X by A1, Th76; then A2: ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by Def3; ((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7; then ((x \ y) \ z) \ (x \ (y \ z)) = ((x \ (x \ (y \ z))) \ y) \ z by Th7; then ((x \ y) \ z) \ (x \ (y \ z)) = (((x \ x) \ (y \ z)) \ y) \ z by A1, Def27; then ((x \ y) \ z) \ (x \ (y \ z)) = (((y \ z) `) \ y) \ z by Def5; then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ z) \ y) \ z by A1, Th76; then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ y) \ z) \ z by Th7; then ((x \ y) \ z) \ (x \ (y \ z)) = (z `) \ z by Def5; then A3: ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by A1, Th76; (x \ (y \ z)) \ ((x \ y) \ z) = (((x \ y) \ y) \ (y \ z)) \ ((x \ y) \ z) by A1, Th76 .= (((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z) by Th7 ; then (x \ (y \ z)) \ ((x \ y) \ z) = 0. X by A2, Th2; hence (x \ y) \ z = x \ (y \ z) by A3, Def7; ::_thesis: verum end; hence X is associative by Def20; ::_thesis: verum end; assume X is associative ; ::_thesis: X is alternative then for x, y being Element of X holds ( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) by Def20; hence X is alternative by Def27; ::_thesis: verum end; Lm22: for X being BCI-algebra st X is alternative holds X is implicative proof let X be BCI-algebra; ::_thesis: ( X is alternative implies X is implicative ) assume X is alternative ; ::_thesis: X is implicative then for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by Th76; hence X is implicative by Def24; ::_thesis: verum end; registration cluster non empty being_B being_C being_I being_BCI-4 alternative -> associative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is alternative holds b1 is associative by Lm21; cluster non empty being_B being_C being_I being_BCI-4 associative -> alternative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is associative holds b1 is alternative by Lm21; cluster non empty being_B being_C being_I being_BCI-4 alternative -> implicative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is alternative holds b1 is implicative by Lm22; end; theorem :: BCIALG_1:81 for X being BCI-algebra for x, y being Element of X st X is alternative holds (x \ (x \ y)) \ (y \ x) = x proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is alternative holds (x \ (x \ y)) \ (y \ x) = x let x, y be Element of X; ::_thesis: ( X is alternative implies (x \ (x \ y)) \ (y \ x) = x ) assume A1: X is alternative ; ::_thesis: (x \ (x \ y)) \ (y \ x) = x then x \ (x \ y) = y by Th76; hence (x \ (x \ y)) \ (y \ x) = x by A1, Th76; ::_thesis: verum end; theorem :: BCIALG_1:82 for X being BCI-algebra for y, x being Element of X st X is alternative holds y \ (y \ (x \ (x \ y))) = y proof let X be BCI-algebra; ::_thesis: for y, x being Element of X st X is alternative holds y \ (y \ (x \ (x \ y))) = y let y, x be Element of X; ::_thesis: ( X is alternative implies y \ (y \ (x \ (x \ y))) = y ) assume X is alternative ; ::_thesis: y \ (y \ (x \ (x \ y))) = y then y \ (y \ (x \ (x \ y))) = y \ (y \ y) by Th76 .= y \ (0. X) by Def5 .= y by Th2 ; hence y \ (y \ (x \ (x \ y))) = y ; ::_thesis: verum end; begin Lm23: for X being BCI-algebra st X is associative holds X is weakly-positive-implicative proof let X be BCI-algebra; ::_thesis: ( X is associative implies X is weakly-positive-implicative ) assume A1: X is associative ; ::_thesis: X is weakly-positive-implicative for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z) (x \ y) \ z = x \ (y \ z) by A1, Def20; then (x \ y) \ z = (x \ (0. X)) \ (y \ z) by Th2; then (x \ y) \ z = (x \ (z \ z)) \ (y \ z) by Def5; hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A1, Def20; ::_thesis: verum end; hence X is weakly-positive-implicative by Def23; ::_thesis: verum end; Lm24: for X being BCI-algebra st X is p-Semisimple BCI-algebra holds X is weakly-positive-implicative BCI-algebra proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative BCI-algebra ) assume A1: X is p-Semisimple BCI-algebra ; ::_thesis: X is weakly-positive-implicative BCI-algebra for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z) ((x \ z) \ z) \ (y \ z) = (x \ z) \ y by A1, Lm12 .= (x \ z) \ (y \ (0. X)) by Th2 .= (x \ y) \ (z \ (0. X)) by A1, Lm10 ; hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by Th2; ::_thesis: verum end; hence X is weakly-positive-implicative BCI-algebra by Def23; ::_thesis: verum end; registration cluster non empty being_B being_C being_I being_BCI-4 associative -> weakly-positive-implicative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is associative holds b1 is weakly-positive-implicative by Lm23; cluster non empty being_B being_C being_I being_BCI-4 p-Semisimple -> weakly-positive-implicative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is p-Semisimple holds b1 is weakly-positive-implicative by Lm24; end; theorem :: BCIALG_1:83 for X being non empty BCIStr_0 holds ( X is implicative BCI-algebra iff for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is implicative BCI-algebra iff for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) thus ( X is implicative BCI-algebra implies for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) by Def24, Th1, Th2; ::_thesis: ( ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra ) thus ( ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ) implies X is implicative BCI-algebra ) ::_thesis: verum proof assume A1: for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & (x \ (x \ y)) \ (y \ x) = y \ (y \ x) ) ; ::_thesis: X is implicative BCI-algebra A2: now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_) let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: (x \ (x \ y)) \ y = 0. X (x \ (x \ y)) \ y = ((x \ (0. X)) \ (x \ y)) \ y by A1 .= ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) by A1 ; hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_ x_=_y let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume that A3: x \ y = 0. X and A4: y \ x = 0. X ; ::_thesis: x = y x = x \ (0. X) by A1 .= (y \ (y \ x)) \ (x \ y) by A1, A3 .= y \ (0. X) by A1, A3, A4 ; hence x = y by A1; ::_thesis: verum end; then A5: X is being_BCI-4 by Def7; now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X let x be Element of X; ::_thesis: x \ x = 0. X x \ x = (x \ (0. X)) \ x by A1 .= (x \ (0. X)) \ (x \ (0. X)) by A1 .= ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) by A1 .= ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) by A1 ; hence x \ x = 0. X by A1; ::_thesis: verum end; then X is being_I by Def5; hence X is implicative BCI-algebra by A1, A5, A2, Def24, Th1; ::_thesis: verum end; end; theorem Th84: :: BCIALG_1:84 for X being BCI-algebra holds ( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) proof let X be BCI-algebra; ::_thesis: ( X is weakly-positive-implicative iff for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) thus ( X is weakly-positive-implicative implies for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ) implies X is weakly-positive-implicative ) proof assume A1: X is weakly-positive-implicative ; ::_thesis: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) let x, y be Element of X; ::_thesis: x \ y = ((x \ y) \ y) \ (y `) (x \ (0. X)) \ y = ((x \ y) \ y) \ (y `) by A1, Def23; hence x \ y = ((x \ y) \ y) \ (y `) by Th2; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) ; ::_thesis: X is weakly-positive-implicative for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = ((x \ z) \ z) \ (y \ z) ((x \ z) \ (y \ z)) \ (x \ y) = 0. X by Def3; then (((x \ z) \ (y \ z)) \ z) \ ((x \ y) \ z) = 0. X by Th4; then A3: (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X by Th7; (((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (y \ z) = 0. X by Th1; then ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ ((y \ z) \ (z `)) = 0. X by Th4; then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ y) = 0. X by Th4; then (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (((y \ z) \ (z `)) \ (y \ (0. X))) = 0. X by Th2; then A4: (((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y) \ (0. X) = 0. X by Def3; ((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = ((x \ z) \ y) \ (((x \ z) \ z) \ (y \ z)) by Th7 .= ((((x \ z) \ z) \ (z `)) \ y) \ (((x \ z) \ z) \ (y \ z)) by A2 .= ((((x \ z) \ z) \ (z `)) \ (((x \ z) \ z) \ (y \ z))) \ y by Th7 .= ((((x \ z) \ z) \ (((x \ z) \ z) \ (y \ z))) \ (z `)) \ y by Th7 ; then ((x \ y) \ z) \ (((x \ z) \ z) \ (y \ z)) = 0. X by A4, Th2; hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A3, Def7; ::_thesis: verum end; hence X is weakly-positive-implicative by Def23; ::_thesis: verum end; Lm25: for X being BCI-algebra for x, y being Element of X st X is weakly-positive-implicative holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) proof let X be BCI-algebra; ::_thesis: for x, y being Element of X st X is weakly-positive-implicative holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) let x, y be Element of X; ::_thesis: ( X is weakly-positive-implicative implies (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) assume A1: X is weakly-positive-implicative ; ::_thesis: (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ((x \ (x \ y)) \ (y \ (x \ y))) \ (x \ y) = 0. X by Def3; then ((x \ (x \ y)) \ (x \ y)) \ (y \ (x \ y)) = 0. X by Th7; then (((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ ((y \ (x \ y)) \ ((x \ y) `)) = 0. X by Th4; then ((((x \ (x \ y)) \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by Th4; then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ ((x \ y) `)) \ (y \ x)) = 0. X by A1, Th84; then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ y) `) \ (y \ x))) = 0. X by A1, Def23; then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (((x \ x) \ (x \ y)) \ (y \ x))) = 0. X by Def5; then ((x \ (x \ y)) \ (y \ x)) \ ((((y \ (x \ y)) \ (y \ x)) \ (y \ x)) \ (0. X)) = 0. X by Th1; then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (x \ y)) \ (y \ x)) \ (y \ x)) = 0. X by Th2; then ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (x \ y)) \ (y \ x)) = 0. X by Th7; then A2: ((x \ (x \ y)) \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) = 0. X by Th7; ((y \ (y \ x)) \ (y \ x)) \ (x \ (y \ x)) = 0. X by Th1; then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (y \ x)) \ (x \ y)) = 0. X by Th4; then (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by Th7; hence (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by A2, Def7; ::_thesis: verum end; Lm26: for X being BCI-algebra holds ( X is positive-implicative iff X is weakly-positive-implicative ) proof let X be BCI-algebra; ::_thesis: ( X is positive-implicative iff X is weakly-positive-implicative ) thus ( X is positive-implicative implies X is weakly-positive-implicative ) ::_thesis: ( X is weakly-positive-implicative implies X is positive-implicative ) proof assume A1: X is positive-implicative ; ::_thesis: X is weakly-positive-implicative for x, y being Element of X holds x \ y = ((x \ y) \ y) \ (y `) proof let x, y be Element of X; ::_thesis: x \ y = ((x \ y) \ y) \ (y `) ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) by A1, Def22; then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ (x \ y)) by Th8; then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = (x \ y) \ (0. X) by Def5; then ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = x \ y by Th2; then ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) = x \ y by Th7; then ((x \ y) \ (x \ (x \ y))) \ ((x \ x) \ y) = x \ y by Th7; then ((x \ (x \ (x \ y))) \ y) \ ((x \ x) \ y) = x \ y by Th7; then ((x \ y) \ y) \ ((x \ x) \ y) = x \ y by Th8; hence x \ y = ((x \ y) \ y) \ (y `) by Def5; ::_thesis: verum end; hence X is weakly-positive-implicative by Th84; ::_thesis: verum end; assume A2: X is weakly-positive-implicative ; ::_thesis: X is positive-implicative for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y)) by A2, Lm25; (y \ (y \ x)) \ x = 0. X by Th1; then (x \ x) \ (x \ (y \ (y \ x))) = 0. X by Th4; then (x \ (y \ (y \ x))) ` = 0. X by Def5; then x \ (x \ (y \ (y \ x))) = ((x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x)))) \ (0. X) by A2, Th84; then x \ (x \ (y \ (y \ x))) = (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) by Th2; then (x \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ (x \ (y \ (y \ x)))) = 0. X by Th1; then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) = 0. X by Th4; then A4: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) = 0. X by Th7; ((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) = ((((y \ (y \ x)) \ (y \ x)) \ ((y \ x) `)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ ((x \ y) \ ((y \ x) `)) by A2, Th84 .= 0. X by Th1 ; then (((y \ (y \ x)) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (x \ (y \ (y \ x)))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by Th4; then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ ((y \ x) `)) \ (x \ (y \ (y \ x)))) = 0. X by A4, Th3; then A5: ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ x) `)) = 0. X by Th7; ((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ (y \ x)) \ y) = 0. X by Th1; then ((x \ y) \ (x \ (y \ (y \ x)))) \ ((y \ y) \ (y \ x)) = 0. X by Th7; then ((x \ (x \ (y \ (y \ x)))) \ (((y \ (y \ x)) \ (y \ x)) \ (x \ y))) \ (0. X) = 0. X by A5, Def5; then A6: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A3, Th2; ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by Th10; hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A6, Def7; ::_thesis: verum end; hence X is positive-implicative by Def22; ::_thesis: verum end; registration cluster non empty being_B being_C being_I being_BCI-4 positive-implicative -> weakly-positive-implicative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is positive-implicative holds b1 is weakly-positive-implicative by Lm26; cluster non empty being_B being_C being_I being_BCI-4 alternative -> weakly-positive-implicative for BCIStr_0 ; coherence for b1 being BCI-algebra st b1 is alternative holds b1 is weakly-positive-implicative ; end; theorem :: BCIALG_1:85 for X being BCI-algebra st X is weakly-positive-implicative BCI-algebra holds for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) by Lm25; theorem :: BCIALG_1:86 for X being non empty BCIStr_0 holds ( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is positive-implicative BCI-algebra iff for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) thus ( X is positive-implicative BCI-algebra implies for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) by Lm25, Th1, Th2, Th84; ::_thesis: ( ( for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ) implies X is positive-implicative BCI-algebra ) assume A1: for x, y, z being Element of X holds ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & x \ (0. X) = x & x \ y = ((x \ y) \ y) \ (y `) & (x \ (x \ y)) \ (y \ x) = ((y \ (y \ x)) \ (y \ x)) \ (x \ y) ) ; ::_thesis: X is positive-implicative BCI-algebra now__::_thesis:_for_x_being_Element_of_X_holds_x_\_x_=_0._X let x be Element of X; ::_thesis: x \ x = 0. X ((x \ (0. X)) \ (x \ (0. X))) \ ((0. X) `) = 0. X by A1; then ((x \ (0. X)) \ (x \ (0. X))) \ (0. X) = 0. X by A1; then ((x \ (0. X)) \ x) \ (0. X) = 0. X by A1; then (x \ x) \ (0. X) = 0. X by A1; hence x \ x = 0. X by A1; ::_thesis: verum end; then A2: X is being_I by Def5; now__::_thesis:_for_x,_y_being_Element_of_X_st_x_\_y_=_0._X_&_y_\_x_=_0._X_holds_ x_=_y 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)) \ (0. X) by A1; then x \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A1; then x = ((y \ (0. X)) \ (0. X)) \ (0. X) by A1; then x = (y \ (0. X)) \ (0. X) by A1; then x = y \ (0. X) by A1; hence x = y by A1; ::_thesis: verum end; then A3: X is being_BCI-4 by Def7; now__::_thesis:_for_x,_y,_z_being_Element_of_X_holds_ (_((x_\_y)_\_(x_\_z))_\_(z_\_y)_=_0._X_&_(x_\_(x_\_y))_\_y_=_0._X_) let x, y, z be Element of X; ::_thesis: ( ((x \ y) \ (x \ z)) \ (z \ y) = 0. X & (x \ (x \ y)) \ y = 0. X ) thus ((x \ y) \ (x \ z)) \ (z \ y) = 0. X by A1; ::_thesis: (x \ (x \ y)) \ y = 0. X ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) = 0. X by A1; then (x \ (x \ y)) \ (y \ (0. X)) = 0. X by A1; hence (x \ (x \ y)) \ y = 0. X by A1; ::_thesis: verum end; then X is weakly-positive-implicative BCI-algebra by A1, A2, A3, Th1, Th84; hence X is positive-implicative BCI-algebra by Lm26; ::_thesis: verum end;