:: BCIALG_3 semantic presentation begin definition let IT be non empty BCIStr_0 ; attrIT is commutative means :Def1: :: BCIALG_3:def 1 for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x); end; :: deftheorem Def1 defines commutative BCIALG_3:def_1_:_ for IT being non empty BCIStr_0 holds ( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) ); registration cluster BCI-EXAMPLE -> commutative ; coherence BCI-EXAMPLE is commutative proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_1 ::_thesis: x \ (x \ y) = y \ (y \ x) thus x \ (x \ y) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative for BCIStr_0 ; existence ex b1 being BCK-algebra st b1 is commutative proof take BCI-EXAMPLE ; ::_thesis: BCI-EXAMPLE is commutative thus BCI-EXAMPLE is commutative ; ::_thesis: verum end; end; theorem Th1: :: BCIALG_3:1 for X being BCK-algebra holds ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) x \ (x \ y) = y \ (y \ x) by A1, Def1; then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def_5; hence x \ (x \ y) <= y \ (y \ x) by BCIALG_1:def_11; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) y \ (y \ x) <= x \ (x \ y) by A2; then A3: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by BCIALG_1:def_11; x \ (x \ y) <= y \ (y \ x) by A2; then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by BCIALG_1:def_11; hence x \ (x \ y) = y \ (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is commutative BCK-algebra by Def1; ::_thesis: verum end; theorem Th2: :: BCIALG_3:2 for X being BCK-algebra for x, y being Element of X holds ( x \ (x \ y) <= y & x \ (x \ y) <= x ) proof let X be BCK-algebra; ::_thesis: for x, y being Element of X holds ( x \ (x \ y) <= y & x \ (x \ y) <= x ) let x, y be Element of X; ::_thesis: ( x \ (x \ y) <= y & x \ (x \ y) <= x ) A1: (0. X) \ (x \ y) = (x \ y) ` .= 0. X by BCIALG_1:def_8 ; ((x \ (x \ y)) \ ((0. X) \ (x \ y))) \ (x \ (0. X)) = 0. X by BCIALG_1:def_3; then ((x \ (x \ y)) \ (0. X)) \ x = 0. X by A1, BCIALG_1:2; then ( (x \ (x \ y)) \ y = 0. X & (x \ (x \ y)) \ x = 0. X ) by BCIALG_1:1, BCIALG_1:2; hence ( x \ (x \ y) <= y & x \ (x \ y) <= x ) by BCIALG_1:def_11; ::_thesis: verum end; theorem Th3: :: BCIALG_3:3 for X being BCK-algebra holds ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ) implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) let x, y be Element of X; ::_thesis: x \ y = x \ (y \ (y \ x)) x \ y = x \ (x \ (x \ y)) by BCIALG_1:8 .= x \ (y \ (y \ x)) by A1, Def1 ; hence x \ y = x \ (y \ (y \ x)) ; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) x \ (x \ (y \ (y \ x))) <= y \ (y \ x) by Th2; hence x \ (x \ y) <= y \ (y \ x) by A2; ::_thesis: verum end; hence X is commutative BCK-algebra by Th1; ::_thesis: verum end; theorem Th4: :: BCIALG_3:4 for X being BCK-algebra holds ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) thus ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y))) y \ (y \ x) = y \ (y \ (x \ (x \ y))) by A1, Th3; hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Def1; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) x \ (x \ y) <= x by Th2; then A3: y \ x <= y \ (x \ (x \ y)) by BCIALG_1:5; x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2; hence x \ (x \ y) <= y \ (y \ x) by A3, BCIALG_1:5; ::_thesis: verum end; hence X is commutative BCK-algebra by Th1; ::_thesis: verum end; theorem Th5: :: BCIALG_3:5 for X being BCK-algebra holds ( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra iff for x, y being Element of X st x <= y holds x = y \ (y \ x) ) thus ( X is commutative BCK-algebra implies for x, y being Element of X st x <= y holds x = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X st x <= y holds x = y \ (y \ x) ) implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X st x <= y holds x = y \ (y \ x) let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) ) assume x <= y ; ::_thesis: x = y \ (y \ x) then x \ y = 0. X by BCIALG_1:def_11; then y \ (y \ x) = x \ (0. X) by A1, Def1 .= x by BCIALG_1:2 ; hence x = y \ (y \ x) ; ::_thesis: verum end; assume A2: for x, y being Element of X st x <= y holds x = y \ (y \ x) ; ::_thesis: X is commutative BCK-algebra for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) (x \ (x \ y)) \ x = (x \ x) \ (x \ y) by BCIALG_1:7 .= (x \ y) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (x \ y) <= x by BCIALG_1:def_11; then A3: y \ x <= y \ (x \ (x \ y)) by BCIALG_1:5; (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then x \ (x \ y) <= y by BCIALG_1:def_11; then x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2; hence x \ (x \ y) <= y \ (y \ x) by A3, BCIALG_1:5; ::_thesis: verum end; hence X is commutative BCK-algebra by Th1; ::_thesis: verum end; theorem Th6: :: BCIALG_3:6 for X being non empty BCIStr_0 holds ( X is commutative BCK-algebra iff for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is commutative BCK-algebra iff for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) thus ( X is commutative BCK-algebra implies for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) ::_thesis: ( ( for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) implies X is commutative BCK-algebra ) proof assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) (x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def1; then A2: (x \ z) \ (x \ y) = (y \ (y \ x)) \ z by A1, BCIALG_1:7 .= (y \ z) \ (y \ x) by A1, BCIALG_1:7 ; (0. X) \ y = y ` .= 0. X by A1, BCIALG_1:def_8 ; hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) by A1, A2, BCIALG_1:2; ::_thesis: verum end; assume A3: for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ; ::_thesis: X is commutative BCK-algebra A4: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) x \ (x \ y) = (x \ ((0. X) \ y)) \ (x \ y) by A3 .= (y \ ((0. X) \ y)) \ (y \ x) by A3 .= y \ (y \ x) by A3 ; hence x \ (x \ y) = y \ (y \ x) ; ::_thesis: verum end; A5: for x, y being Element of X holds x \ (0. X) = x proof let x, y be Element of X; ::_thesis: x \ (0. X) = x (0. X) \ ((0. X) \ (0. X)) = 0. X by A3; hence x \ (0. X) = x by A3; ::_thesis: verum end; for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds x = y proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume ( x \ y = 0. X & y \ x = 0. X ) ; ::_thesis: x = y then (x \ (0. X)) \ (0. X) = (y \ (0. X)) \ (0. X) by A3; then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5 .= y \ (0. X) by A5 ; hence x = y \ (0. X) by A5 .= y by A5 ; ::_thesis: verum end; then A6: X is being_BCI-4 by BCIALG_1:def_7; A7: for x being Element of X holds x \ x = 0. X proof let x be Element of X; ::_thesis: x \ x = 0. X x = x \ (0. X) by A5; then x \ x = ((0. X) \ (0. X)) \ ((0. X) \ x) by A3 .= (0. X) \ ((0. X) \ x) by A5 .= 0. X by A3 ; hence x \ x = 0. X ; ::_thesis: verum end; A8: for x being Element of X holds (0. X) \ x = 0. X proof let x be Element of X; ::_thesis: (0. X) \ x = 0. X 0. X = ((0. X) \ x) \ ((0. X) \ x) by A7 .= (0. X) \ x by A3 ; hence (0. X) \ x = 0. X ; ::_thesis: verum end; A9: for x, y, z being Element of X holds ((x \ y) \ (x \ z)) \ (z \ y) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3 .= ((z \ y) \ (z \ x)) \ ((z \ y) \ (0. X)) by A5 .= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3 .= (0. X) \ ((0. X) \ (z \ y)) by A8 .= 0. X by A8 ; hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; ::_thesis: verum end; A10: for x, y being Element of X holds (x \ (x \ y)) \ y = 0. X proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ y = 0. X 0. X = ((x \ (0. X)) \ (x \ y)) \ (y \ (0. X)) by A9 .= (x \ (x \ y)) \ (y \ (0. X)) by A5 .= (x \ (x \ y)) \ y by A5 ; hence (x \ (x \ y)) \ y = 0. X ; ::_thesis: verum end; A11: X is being_I by A7, BCIALG_1:def_5; for x being Element of X holds x ` = 0. X by A8; hence X is commutative BCK-algebra by A4, A9, A10, A11, A6, Def1, BCIALG_1:1, BCIALG_1:def_8; ::_thesis: verum end; theorem :: BCIALG_3:7 for X being BCK-algebra st X is commutative BCK-algebra holds for x, y being Element of X st x \ y = x holds y \ x = y proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X st x \ y = x holds y \ x = y ) assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X st x \ y = x holds y \ x = y let x, y be Element of X; ::_thesis: ( x \ y = x implies y \ x = y ) assume x \ y = x ; ::_thesis: y \ x = y then y \ (y \ x) = x \ x by A1, Def1 .= 0. X by BCIALG_1:def_5 ; then y \ x = y \ (0. X) by BCIALG_1:8 .= y by BCIALG_1:2 ; hence y \ x = y ; ::_thesis: verum end; theorem Th8: :: BCIALG_3:8 for X being BCK-algebra st X is commutative BCK-algebra holds for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x ) assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y, a being Element of X st y <= a holds (a \ x) \ (a \ y) = y \ x let x, y, a be Element of X; ::_thesis: ( y <= a implies (a \ x) \ (a \ y) = y \ x ) assume y <= a ; ::_thesis: (a \ x) \ (a \ y) = y \ x then A2: y \ a = 0. X by BCIALG_1:def_11; (a \ x) \ (a \ y) = (a \ (a \ y)) \ x by BCIALG_1:7 .= (y \ (0. X)) \ x by A1, A2, Def1 .= y \ x by BCIALG_1:2 ; hence (a \ x) \ (a \ y) = y \ x ; ::_thesis: verum end; theorem :: BCIALG_3:9 for X being BCK-algebra st X is commutative BCK-algebra holds for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) ) assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) A2: for x, y being Element of X st y \ (y \ x) = 0. X holds x \ y = x proof let x, y be Element of X; ::_thesis: ( y \ (y \ x) = 0. X implies x \ y = x ) assume A3: y \ (y \ x) = 0. X ; ::_thesis: x \ y = x x \ y = x \ (x \ (x \ y)) by BCIALG_1:8 .= x \ (0. X) by A1, A3, Def1 .= x by BCIALG_1:2 ; hence x \ y = x ; ::_thesis: verum end; for x, y being Element of X st x \ y = x holds y \ (y \ x) = 0. X proof let x, y be Element of X; ::_thesis: ( x \ y = x implies y \ (y \ x) = 0. X ) assume x \ y = x ; ::_thesis: y \ (y \ x) = 0. X then y \ (y \ x) = x \ x by A1, Def1 .= 0. X by BCIALG_1:def_5 ; hence y \ (y \ x) = 0. X ; ::_thesis: verum end; hence for x, y being Element of X holds ( x \ y = x iff y \ (y \ x) = 0. X ) by A2; ::_thesis: verum end; theorem :: BCIALG_3:10 for X being BCK-algebra st X is commutative BCK-algebra holds for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) proof let X be BCK-algebra; ::_thesis: ( X is commutative BCK-algebra implies for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) assume A1: X is commutative BCK-algebra ; ::_thesis: for x, y being Element of X holds ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) let x, y be Element of X; ::_thesis: ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) A2: (x \ y) \ ((x \ y) \ x) = x \ (x \ (x \ y)) by A1, Def1 .= x \ y by BCIALG_1:8 ; x \ (y \ (y \ x)) = x \ (x \ (x \ y)) by A1, Def1 .= x \ y by BCIALG_1:8 ; hence ( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) by A2; ::_thesis: verum end; theorem :: BCIALG_3:11 for X being BCK-algebra st X is commutative BCK-algebra holds for x, y, a being Element of X st x <= a holds (a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8; definition let X be BCI-algebra; let a be Element of X; attra is being_greatest means :Def2: :: BCIALG_3:def 2 for x being Element of X holds x \ a = 0. X; attra is being_positive means :: BCIALG_3:def 3 (0. X) \ a = 0. X; end; :: deftheorem Def2 defines being_greatest BCIALG_3:def_2_:_ for X being BCI-algebra for a being Element of X holds ( a is being_greatest iff for x being Element of X holds x \ a = 0. X ); :: deftheorem defines being_positive BCIALG_3:def_3_:_ for X being BCI-algebra for a being Element of X holds ( a is being_positive iff (0. X) \ a = 0. X ); begin definition let IT be BCI-algebra; attrIT is BCI-commutative means :Def4: :: BCIALG_3:def 4 for x, y being Element of IT st x \ y = 0. IT holds x = y \ (y \ x); attrIT is BCI-weakly-commutative means :Def5: :: BCIALG_3:def 5 for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x); end; :: deftheorem Def4 defines BCI-commutative BCIALG_3:def_4_:_ for IT being BCI-algebra holds ( IT is BCI-commutative iff for x, y being Element of IT st x \ y = 0. IT holds x = y \ (y \ x) ); :: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def_5_:_ for IT being BCI-algebra holds ( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) ); registration cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative ; coherence ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative ) proof set IT = BCI-EXAMPLE ; thus BCI-EXAMPLE is BCI-commutative ::_thesis: BCI-EXAMPLE is BCI-weakly-commutative proof let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) ) thus ( x \ y = 0. BCI-EXAMPLE implies x = y \ (y \ x) ) by STRUCT_0:def_10; ::_thesis: verum end; let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_5 ::_thesis: (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x) thus (x \ (x \ y)) \ ((0. BCI-EXAMPLE) \ (x \ y)) = y \ (y \ x) by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 BCI-commutative BCI-weakly-commutative for BCIStr_0 ; existence ex b1 being BCI-algebra st ( b1 is BCI-commutative & b1 is BCI-weakly-commutative ) proof take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative ) thus ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative ) ; ::_thesis: verum end; end; theorem :: BCIALG_3:12 for X being BCI-algebra st ex a being Element of X st a is being_greatest holds X is BCK-algebra proof let X be BCI-algebra; ::_thesis: ( ex a being Element of X st a is being_greatest implies X is BCK-algebra ) given a being Element of X such that A1: a is being_greatest ; ::_thesis: X is BCK-algebra for x being Element of X holds x ` = 0. X proof let x be Element of X; ::_thesis: x ` = 0. X x \ a = 0. X by A1, Def2; then x ` = (x \ x) \ a by BCIALG_1:7 .= 0. X by A1, Def2 ; hence x ` = 0. X ; ::_thesis: verum end; hence X is BCK-algebra by BCIALG_1:def_8; ::_thesis: verum end; theorem :: BCIALG_3:13 for X being BCI-algebra st X is p-Semisimple holds ( X is BCI-commutative & X is BCI-weakly-commutative ) proof let X be BCI-algebra; ::_thesis: ( X is p-Semisimple implies ( X is BCI-commutative & X is BCI-weakly-commutative ) ) assume A1: X is p-Semisimple ; ::_thesis: ( X is BCI-commutative & X is BCI-weakly-commutative ) A2: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) (0. X) \ (x \ y) = ((0. X) \ (0. X)) \ (x \ y) by BCIALG_1:def_5 .= ((0. X) \ x) \ ((0. X) \ y) by A1, BCIALG_1:64 .= (y \ x) \ ((0. X) \ (0. X)) by A1, BCIALG_1:58 .= (y \ x) \ (0. X) by BCIALG_1:def_5 .= y \ x by BCIALG_1:2 ; hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A1, BCIALG_1:def_26; ::_thesis: verum end; for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) by A1, BCIALG_1:def_26; hence ( X is BCI-commutative & X is BCI-weakly-commutative ) by A2, Def4, Def5; ::_thesis: verum end; theorem :: BCIALG_3:14 for X being commutative BCK-algebra holds ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra ) proof let X be commutative BCK-algebra; ::_thesis: ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra ) A1: for x, y being Element of X holds (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) A2: (0. X) \ (x \ y) = (x \ y) ` .= 0. X by BCIALG_1:def_8 ; x \ (x \ y) = y \ (y \ x) by Def1; hence (x \ (x \ y)) \ ((0. X) \ (x \ y)) = y \ (y \ x) by A2, BCIALG_1:2; ::_thesis: verum end; for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then x <= y by BCIALG_1:def_11; hence x = y \ (y \ x) by Th5; ::_thesis: verum end; hence ( X is BCI-commutative BCI-algebra & X is BCI-weakly-commutative BCI-algebra ) by A1, Def4, Def5; ::_thesis: verum end; theorem :: BCIALG_3:15 for X being BCK-algebra st X is BCI-weakly-commutative BCI-algebra holds X is BCI-commutative proof let X be BCK-algebra; ::_thesis: ( X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative ) assume A1: X is BCI-weakly-commutative BCI-algebra ; ::_thesis: X is BCI-commutative let x, y be Element of X; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then (x \ (0. X)) \ ((0. X) \ (0. X)) = y \ (y \ x) by A1, Def5; then (x \ (0. X)) \ (0. X) = y \ (y \ x) by BCIALG_1:def_5; then x \ (0. X) = y \ (y \ x) by BCIALG_1:2; hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum end; theorem Th16: :: BCIALG_3:16 for X being BCI-algebra holds ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) A1: ( ( for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is BCI-commutative ) proof assume A2: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is BCI-commutative let x, y be Element of X; :: according to BCIALG_3:def_4 ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then x \ (x \ y) = x by BCIALG_1:2; hence x = y \ (y \ x) by A2; ::_thesis: verum end; ( X is BCI-commutative implies for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof assume A3: X is BCI-commutative ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y))) (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A3, Def4; ::_thesis: verum end; hence ( X is BCI-commutative iff for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ) by A1; ::_thesis: verum end; theorem Th17: :: BCIALG_3:17 for X being BCI-algebra holds ( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) A1: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) implies X is BCI-commutative ) proof assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ; ::_thesis: X is BCI-commutative for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) A3: (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; assume A4: x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then 0. X = (0. X) \ (x \ y) by BCIALG_1:2 .= (x \ (0. X)) \ (y \ (y \ x)) by A2, A4 .= x \ (y \ (y \ x)) by BCIALG_1:2 ; hence x = y \ (y \ x) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCI-commutative by Def4; ::_thesis: verum end; ( X is BCI-commutative implies for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) proof assume A5: X is BCI-commutative ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) (x \ (x \ y)) \ (y \ (y \ x)) = (y \ (y \ (x \ (x \ y)))) \ (y \ (y \ x)) by A5, Th16 .= (y \ (y \ (y \ x))) \ (y \ (x \ (x \ y))) by BCIALG_1:7 .= (y \ x) \ (y \ (x \ (x \ y))) by BCIALG_1:8 .= (y \ (y \ (x \ (x \ y)))) \ x by BCIALG_1:7 .= (x \ (x \ y)) \ x by A5, Th16 .= (x \ x) \ (x \ y) by BCIALG_1:7 ; hence (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) by BCIALG_1:def_5; ::_thesis: verum end; hence ( X is BCI-commutative iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ (y \ x)) = (0. X) \ (x \ y) ) by A1; ::_thesis: verum end; theorem :: BCIALG_3:18 for X being BCI-algebra holds ( X is BCI-commutative iff for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) thus ( X is BCI-commutative implies for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) ::_thesis: ( ( for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ) implies X is BCI-commutative ) proof assume A1: X is BCI-commutative ; ::_thesis: for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) let a be Element of AtomSet X; ::_thesis: for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) let x, y be Element of BranchV a; ::_thesis: x \ (x \ y) = y \ (y \ x) y \ x in BranchV (a \ a) by BCIALG_1:39; then ex z1 being Element of X st ( y \ x = z1 & a \ a <= z1 ) ; then 0. X <= y \ x by BCIALG_1:def_5; then (0. X) \ (y \ x) = 0. X by BCIALG_1:def_11; then A2: (y \ (y \ x)) \ (x \ (x \ y)) = 0. X by A1, Th17; x \ y in BranchV (a \ a) by BCIALG_1:39; then ex z being Element of X st ( x \ y = z & a \ a <= z ) ; then 0. X <= x \ y by BCIALG_1:def_5; then (0. X) \ (x \ y) = 0. X by BCIALG_1:def_11; then (x \ (x \ y)) \ (y \ (y \ x)) = 0. X by A1, Th17; hence x \ (x \ y) = y \ (y \ x) by A2, BCIALG_1:def_7; ::_thesis: verum end; assume A3: for a being Element of AtomSet X for x, y being Element of BranchV a holds x \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCI-commutative for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) set aa = (0. X) \ ((0. X) \ x); (((0. X) \ ((0. X) \ x)) `) ` = (0. X) \ ((0. X) \ x) by BCIALG_1:8; then A4: (0. X) \ ((0. X) \ x) in AtomSet X by BCIALG_1:29; A5: ((0. X) \ ((0. X) \ x)) \ x = ((0. X) \ x) \ ((0. X) \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then A6: (0. X) \ ((0. X) \ x) <= x by BCIALG_1:def_11; assume A7: x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then ((0. X) \ ((0. X) \ x)) \ y = 0. X by A5, BCIALG_1:3; then (0. X) \ ((0. X) \ x) <= y by BCIALG_1:def_11; then consider aa being Element of AtomSet X such that A8: ( aa <= x & aa <= y ) by A4, A6; ( x in BranchV aa & y in BranchV aa ) by A8; then x \ (x \ y) = y \ (y \ x) by A3; hence x = y \ (y \ x) by A7, BCIALG_1:2; ::_thesis: verum end; hence X is BCI-commutative by Def4; ::_thesis: verum end; theorem :: BCIALG_3:19 for X being non empty BCIStr_0 holds ( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) ) ( ( 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 \ (y \ (x \ (x \ y))) ) ) implies X is BCI-commutative BCI-algebra ) 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 \ (y \ (x \ (x \ y))) ) ; ::_thesis: X is BCI-commutative BCI-algebra 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 A2: x \ y = 0. X and A3: y \ x = 0. X ; ::_thesis: x = y A4: x \ (x \ y) = x by A1, A2; y \ (y \ (x \ (x \ y))) = y \ (0. X) by A1, A2, A3 .= y by A1 ; hence x = y by A1, A4; ::_thesis: verum end; then X is being_BCI-4 by BCIALG_1:def_7; hence X is BCI-commutative BCI-algebra by A1, Th16, BCIALG_1:11; ::_thesis: verum end; hence ( X is BCI-commutative 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 \ (y \ (x \ (x \ y))) ) ) by Th16, BCIALG_1:1, BCIALG_1:2; ::_thesis: verum end; theorem :: BCIALG_3:20 for X being BCI-algebra holds ( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ) A1: ( ( for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ) implies X is BCI-commutative ) proof assume A2: for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ; ::_thesis: X is BCI-commutative for x, z being Element of X st x \ z = 0. X holds x = z \ (z \ x) proof let x, z be Element of X; ::_thesis: ( x \ z = 0. X implies x = z \ (z \ x) ) set y = z \ (z \ x); (z \ (z \ (z \ x))) \ (z \ x) = (z \ x) \ (z \ x) by BCIALG_1:8 .= 0. X by BCIALG_1:def_5 ; then A3: z \ (z \ (z \ x)) <= z \ x by BCIALG_1:def_11; assume x \ z = 0. X ; ::_thesis: x = z \ (z \ x) then x <= z by BCIALG_1:def_11; then x <= z \ (z \ x) by A2, A3; then A4: x \ (z \ (z \ x)) = 0. X by BCIALG_1:def_11; (z \ (z \ x)) \ x = (z \ x) \ (z \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence x = z \ (z \ x) by A4, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCI-commutative by Def4; ::_thesis: verum end; ( X is BCI-commutative implies for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ) proof assume A5: X is BCI-commutative ; ::_thesis: for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y proof let x, y, z be Element of X; ::_thesis: ( x <= z & z \ y <= z \ x implies x <= y ) assume that A6: x <= z and A7: z \ y <= z \ x ; ::_thesis: x <= y x \ z = 0. X by A6, BCIALG_1:def_11; then A8: x = z \ (z \ x) by A5, Def4; (z \ y) \ (z \ x) = 0. X by A7, BCIALG_1:def_11; then 0. X = x \ y by A8, BCIALG_1:7; hence x <= y by BCIALG_1:def_11; ::_thesis: verum end; hence for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ; ::_thesis: verum end; hence ( X is BCI-commutative iff for x, y, z being Element of X st x <= z & z \ y <= z \ x holds x <= y ) by A1; ::_thesis: verum end; theorem :: BCIALG_3:21 for X being BCI-algebra holds ( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ) proof let X be BCI-algebra; ::_thesis: ( X is BCI-commutative iff for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ) thus ( X is BCI-commutative implies for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ) ::_thesis: ( ( for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ) implies X is BCI-commutative ) proof assume A1: X is BCI-commutative ; ::_thesis: for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) proof let x, y, z be Element of X; ::_thesis: ( x <= y & x <= z implies x <= y \ (y \ z) ) assume that A2: x <= y and A3: x <= z ; ::_thesis: x <= y \ (y \ z) A4: x \ z = 0. X by A3, BCIALG_1:def_11; x \ y = 0. X by A2, BCIALG_1:def_11; then A5: x = y \ (y \ x) by A1, Def4; then x \ (y \ (y \ z)) = (y \ (y \ (y \ z))) \ (y \ x) by BCIALG_1:7 .= (y \ z) \ (y \ x) by BCIALG_1:8 .= 0. X by A4, A5, BCIALG_1:7 ; hence x <= y \ (y \ z) by BCIALG_1:def_11; ::_thesis: verum end; hence for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ; ::_thesis: verum end; assume A6: for x, y, z being Element of X st x <= y & x <= z holds x <= y \ (y \ z) ; ::_thesis: X is BCI-commutative for x, y being Element of X st x \ y = 0. X holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X implies x = y \ (y \ x) ) x \ x = 0. X by BCIALG_1:def_5; then A7: x <= x by BCIALG_1:def_11; assume x \ y = 0. X ; ::_thesis: x = y \ (y \ x) then x <= y by BCIALG_1:def_11; then x <= y \ (y \ x) by A6, A7; then A8: x \ (y \ (y \ x)) = 0. X by BCIALG_1:def_11; (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence x = y \ (y \ x) by A8, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCI-commutative by Def4; ::_thesis: verum end; begin definition let IT be BCK-algebra; attrIT is bounded means :: BCIALG_3:def 6 ex a being Element of IT st a is being_greatest ; end; :: deftheorem defines bounded BCIALG_3:def_6_:_ for IT being BCK-algebra holds ( IT is bounded iff ex a being Element of IT st a is being_greatest ); registration cluster BCI-EXAMPLE -> bounded ; coherence BCI-EXAMPLE is bounded proof set IT = BCI-EXAMPLE ; set a = the Element of BCI-EXAMPLE; BCI-EXAMPLE is bounded proof take the Element of BCI-EXAMPLE ; :: according to BCIALG_3:def_6 ::_thesis: the Element of BCI-EXAMPLE is being_greatest for x being Element of BCI-EXAMPLE holds x \ the Element of BCI-EXAMPLE = 0. BCI-EXAMPLE by STRUCT_0:def_10; hence the Element of BCI-EXAMPLE is being_greatest by Def2; ::_thesis: verum end; hence BCI-EXAMPLE is bounded ; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded for BCIStr_0 ; existence ex b1 being BCK-algebra st ( b1 is bounded & b1 is commutative ) proof take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) thus ( BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) ; ::_thesis: verum end; end; definition let IT be bounded BCK-algebra; attrIT is involutory means :Def7: :: BCIALG_3:def 7 for a being Element of IT st a is being_greatest holds for x being Element of IT holds a \ (a \ x) = x; end; :: deftheorem Def7 defines involutory BCIALG_3:def_7_:_ for IT being bounded BCK-algebra holds ( IT is involutory iff for a being Element of IT st a is being_greatest holds for x being Element of IT holds a \ (a \ x) = x ); theorem Th22: :: BCIALG_3:22 for X being bounded BCK-algebra holds ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) proof let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) thus ( X is involutory implies for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) implies X is involutory ) proof assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ) assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) proof let x, y be Element of X; ::_thesis: x \ y = (a \ y) \ (a \ x) x \ y = (a \ (a \ x)) \ y by A1, A2, Def7 .= (a \ y) \ (a \ x) by BCIALG_1:7 ; hence x \ y = (a \ y) \ (a \ x) ; ::_thesis: verum end; hence for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; ::_thesis: verum end; assume A3: for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ y = (a \ y) \ (a \ x) ; ::_thesis: X is involutory let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x ) assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x now__::_thesis:_for_x_being_Element_of_X_holds_a_\_(a_\_x)_=_x let x be Element of X; ::_thesis: a \ (a \ x) = x (a \ (a \ x)) \ (0. X) = (a \ (0. X)) \ (a \ x) by BCIALG_1:7 .= x \ (0. X) by A3, A4 .= x by BCIALG_1:2 ; hence a \ (a \ x) = x by BCIALG_1:2; ::_thesis: verum end; hence for x being Element of X holds a \ (a \ x) = x ; ::_thesis: verum end; theorem Th23: :: BCIALG_3:23 for X being bounded BCK-algebra holds ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) proof let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) thus ( X is involutory implies for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) implies X is involutory ) proof assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ) assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) let x, y be Element of X; ::_thesis: x \ (a \ y) = y \ (a \ x) ( x \ (a \ y) = (a \ (a \ y)) \ (a \ x) & y \ (a \ x) = (a \ (a \ x)) \ (a \ y) ) by A1, A2, Th22; hence x \ (a \ y) = y \ (a \ x) by BCIALG_1:7; ::_thesis: verum end; assume A3: for a being Element of X st a is being_greatest holds for x, y being Element of X holds x \ (a \ y) = y \ (a \ x) ; ::_thesis: X is involutory let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x ) assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x let x be Element of X; ::_thesis: a \ (a \ x) = x a \ (a \ x) = x \ (a \ a) by A3, A4 .= x \ (0. X) by BCIALG_1:def_5 .= x by BCIALG_1:2 ; hence a \ (a \ x) = x ; ::_thesis: verum end; theorem :: BCIALG_3:24 for X being bounded BCK-algebra holds ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x ) proof let X be bounded BCK-algebra; ::_thesis: ( X is involutory iff for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x ) thus ( X is involutory implies for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x ) ::_thesis: ( ( for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x ) implies X is involutory ) proof assume A1: X is involutory ; ::_thesis: for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x let a be Element of X; ::_thesis: ( a is being_greatest implies for x, y being Element of X st x <= a \ y holds y <= a \ x ) assume A2: a is being_greatest ; ::_thesis: for x, y being Element of X st x <= a \ y holds y <= a \ x let x, y be Element of X; ::_thesis: ( x <= a \ y implies y <= a \ x ) assume x <= a \ y ; ::_thesis: y <= a \ x then x \ (a \ y) = 0. X by BCIALG_1:def_11; then y \ (a \ x) = 0. X by A1, A2, Th23; hence y <= a \ x by BCIALG_1:def_11; ::_thesis: verum end; assume A3: for a being Element of X st a is being_greatest holds for x, y being Element of X st x <= a \ y holds y <= a \ x ; ::_thesis: X is involutory let a be Element of X; :: according to BCIALG_3:def_7 ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x ) assume A4: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x let x be Element of X; ::_thesis: a \ (a \ x) = x (a \ x) \ (a \ x) = 0. X by BCIALG_1:def_5; then a \ x <= a \ x by BCIALG_1:def_11; then x <= a \ (a \ x) by A3, A4; then A5: x \ (a \ (a \ x)) = 0. X by BCIALG_1:def_11; (a \ (a \ x)) \ x = (a \ x) \ (a \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; hence a \ (a \ x) = x by A5, BCIALG_1:def_7; ::_thesis: verum end; definition let IT be BCK-algebra; let a be Element of IT; attra is being_Iseki means :Def8: :: BCIALG_3:def 8 for x being Element of IT holds ( x \ a = 0. IT & a \ x = a ); end; :: deftheorem Def8 defines being_Iseki BCIALG_3:def_8_:_ for IT being BCK-algebra for a being Element of IT holds ( a is being_Iseki iff for x being Element of IT holds ( x \ a = 0. IT & a \ x = a ) ); definition let IT be BCK-algebra; attrIT is Iseki_extension means :: BCIALG_3:def 9 ex a being Element of IT st a is being_Iseki ; end; :: deftheorem defines Iseki_extension BCIALG_3:def_9_:_ for IT being BCK-algebra holds ( IT is Iseki_extension iff ex a being Element of IT st a is being_Iseki ); registration cluster BCI-EXAMPLE -> Iseki_extension ; coherence BCI-EXAMPLE is Iseki_extension proof set IT = BCI-EXAMPLE ; BCI-EXAMPLE is Iseki_extension proof set a = the Element of BCI-EXAMPLE; take the Element of BCI-EXAMPLE ; :: according to BCIALG_3:def_9 ::_thesis: the Element of BCI-EXAMPLE is being_Iseki for x being Element of BCI-EXAMPLE holds ( x \ the Element of BCI-EXAMPLE = 0. BCI-EXAMPLE & the Element of BCI-EXAMPLE \ x = the Element of BCI-EXAMPLE ) by STRUCT_0:def_10; hence the Element of BCI-EXAMPLE is being_Iseki by Def8; ::_thesis: verum end; hence BCI-EXAMPLE is Iseki_extension ; ::_thesis: verum end; end; definition let X be BCK-algebra; mode Commutative-Ideal of X -> non empty Subset of X means :Def10: :: BCIALG_3:def 10 ( 0. X in it & ( for x, y, z being Element of X st (x \ y) \ z in it & z in it holds x \ (y \ (y \ x)) in it ) ); existence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & z in b1 holds x \ (y \ (y \ x)) in b1 ) ) proof set X1 = BCK-part X; A1: for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds x \ (y \ (y \ x)) in BCK-part X proof let x, y, z be Element of X; ::_thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X ) assume that (x \ y) \ z in BCK-part X and z in BCK-part X ; ::_thesis: x \ (y \ (y \ x)) in BCK-part X (0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) ` .= 0. X by BCIALG_1:def_8 ; then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def_11; hence x \ (y \ (y \ x)) in BCK-part X ; ::_thesis: verum end; 0. X in BCK-part X by BCIALG_1:19; hence ex b1 being non empty Subset of X st ( 0. X in b1 & ( for x, y, z being Element of X st (x \ y) \ z in b1 & z in b1 holds x \ (y \ (y \ x)) in b1 ) ) by A1; ::_thesis: verum end; end; :: deftheorem Def10 defines Commutative-Ideal BCIALG_3:def_10_:_ for X being BCK-algebra for b2 being non empty Subset of X holds ( b2 is Commutative-Ideal of X iff ( 0. X in b2 & ( for x, y, z being Element of X st (x \ y) \ z in b2 & z in b2 holds x \ (y \ (y \ x)) in b2 ) ) ); theorem :: BCIALG_3:25 for X being BCK-algebra for IT being non empty Subset of X st IT is Commutative-Ideal of X holds for x, y being Element of X st x \ y in IT holds x \ (y \ (y \ x)) in IT proof let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds for x, y being Element of X st x \ y in IT holds x \ (y \ (y \ x)) in IT let IT be non empty Subset of X; ::_thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ y in IT holds x \ (y \ (y \ x)) in IT ) assume A1: IT is Commutative-Ideal of X ; ::_thesis: for x, y being Element of X st x \ y in IT holds x \ (y \ (y \ x)) in IT let x, y be Element of X; ::_thesis: ( x \ y in IT implies x \ (y \ (y \ x)) in IT ) assume x \ y in IT ; ::_thesis: x \ (y \ (y \ x)) in IT then A2: (x \ y) \ (0. X) in IT by BCIALG_1:2; thus x \ (y \ (y \ x)) in IT by A1, A2, Def10; ::_thesis: verum end; theorem Th26: :: BCIALG_3:26 for X being BCK-algebra for IT being non empty Subset of X for X being BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X proof let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X for X being BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X let IT be non empty Subset of X; ::_thesis: for X being BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X let X be BCK-algebra; ::_thesis: ( IT is Commutative-Ideal of X implies IT is Ideal of X ) assume A1: IT is Commutative-Ideal of X ; ::_thesis: IT is Ideal of X A2: for x, y being Element of X st x \ y in IT & y in IT holds x in IT proof let x, y be Element of X; ::_thesis: ( x \ y in IT & y in IT implies x in IT ) assume that A3: x \ y in IT and A4: y in IT ; ::_thesis: x in IT A5: x \ ((0. X) \ ((0. X) \ x)) = x \ ((0. X) \ (x `)) .= x \ ((0. X) \ (0. X)) by BCIALG_1:def_8 .= x \ (0. X) by BCIALG_1:def_5 .= x by BCIALG_1:2 ; (x \ (0. X)) \ y in IT by A3, BCIALG_1:2; hence x in IT by A1, A4, A5, Def10; ::_thesis: verum end; 0. X in IT by A1, Def10; hence IT is Ideal of X by A1, A2, BCIALG_1:def_18; ::_thesis: verum end; theorem :: BCIALG_3:27 for X being BCK-algebra for IT being non empty Subset of X st IT is Commutative-Ideal of X holds for x, y being Element of X st x \ (x \ y) in IT holds (y \ (y \ x)) \ (x \ y) in IT proof let X be BCK-algebra; ::_thesis: for IT being non empty Subset of X st IT is Commutative-Ideal of X holds for x, y being Element of X st x \ (x \ y) in IT holds (y \ (y \ x)) \ (x \ y) in IT let IT be non empty Subset of X; ::_thesis: ( IT is Commutative-Ideal of X implies for x, y being Element of X st x \ (x \ y) in IT holds (y \ (y \ x)) \ (x \ y) in IT ) assume IT is Commutative-Ideal of X ; ::_thesis: for x, y being Element of X st x \ (x \ y) in IT holds (y \ (y \ x)) \ (x \ y) in IT then A1: IT is Ideal of X by Th26; let x, y be Element of X; ::_thesis: ( x \ (x \ y) in IT implies (y \ (y \ x)) \ (x \ y) in IT ) ((y \ (y \ x)) \ (x \ y)) \ (x \ (x \ y)) = ((y \ (x \ y)) \ (y \ x)) \ (x \ (x \ y)) by BCIALG_1:7 .= 0. X by BCIALG_1:11 ; then A2: (y \ (y \ x)) \ (x \ y) <= x \ (x \ y) by BCIALG_1:def_11; assume x \ (x \ y) in IT ; ::_thesis: (y \ (y \ x)) \ (x \ y) in IT hence (y \ (y \ x)) \ (x \ y) in IT by A1, A2, BCIALG_1:46; ::_thesis: verum end; begin definition let IT be BCK-algebra; attrIT is BCK-positive-implicative means :Def11: :: BCIALG_3:def 11 for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z); attrIT is BCK-implicative means :Def12: :: BCIALG_3:def 12 for x, y being Element of IT holds x \ (y \ x) = x; end; :: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def_11_:_ for IT being BCK-algebra holds ( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) ); :: deftheorem Def12 defines BCK-implicative BCIALG_3:def_12_:_ for IT being BCK-algebra holds ( IT is BCK-implicative iff for x, y being Element of IT holds x \ (y \ x) = x ); registration cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative ; coherence ( BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative ) proof set IT = BCI-EXAMPLE ; thus BCI-EXAMPLE is BCK-positive-implicative ::_thesis: BCI-EXAMPLE is BCK-implicative proof let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_11 ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z) thus (x \ y) \ z = (x \ z) \ (y \ z) by STRUCT_0:def_10; ::_thesis: verum end; let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_3:def_12 ::_thesis: x \ (y \ x) = x thus x \ (y \ x) = x by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty being_B being_C being_I being_BCI-4 being_BCK-5 commutative bounded Iseki_extension BCK-positive-implicative BCK-implicative for BCIStr_0 ; existence ex b1 being BCK-algebra st ( b1 is Iseki_extension & b1 is BCK-positive-implicative & b1 is BCK-implicative & b1 is bounded & b1 is commutative ) proof take BCI-EXAMPLE ; ::_thesis: ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) thus ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) ; ::_thesis: verum end; end; theorem Th28: :: BCIALG_3:28 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ y ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y = (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ y ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ y let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y (x \ y) \ y = (x \ y) \ (y \ y) by A1, Def11 .= (x \ y) \ (0. X) by BCIALG_1:def_5 .= x \ y by BCIALG_1:2 ; hence x \ y = (x \ y) \ y ; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ y = (x \ y) \ y ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ (y \ z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z) (y \ z) \ y = (y \ y) \ z by BCIALG_1:7 .= z ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then y \ z <= y by BCIALG_1:def_11; then (x \ z) \ y <= (x \ z) \ (y \ z) by BCIALG_1:5; then ((x \ z) \ y) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:def_11; then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7; ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = (((x \ z) \ z) \ (y \ z)) \ ((x \ y) \ z) by A2 .= (((x \ z) \ z) \ (y \ z)) \ ((x \ z) \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_3 ; hence (x \ y) \ z = (x \ z) \ (y \ z) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Def11; ::_thesis: verum end; theorem Th29: :: BCIALG_3:29 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) 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))) (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then x \ (x \ y) <= y by BCIALG_1:def_11; then A2: (x \ (x \ y)) \ (y \ (y \ x)) <= y \ (y \ (y \ x)) by BCIALG_1:5; (x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) = (x \ (x \ (x \ (y \ (y \ x))))) \ (x \ y) by BCIALG_1:7 .= (x \ (y \ (y \ x))) \ (x \ y) by BCIALG_1:8 .= (x \ (x \ y)) \ (y \ (y \ x)) by BCIALG_1:7 ; then (x \ (x \ y)) \ (x \ (x \ (y \ (y \ x)))) <= y \ x by A2, BCIALG_1:8; then ((x \ (x \ y)) \ (x \ (x \ (y \ (y \ x))))) \ (y \ x) = 0. X by BCIALG_1:def_11; then A3: ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:7; (y \ (y \ x)) \ x = (y \ x) \ (y \ x) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then y \ (y \ x) <= x by BCIALG_1:def_11; then (y \ (y \ x)) \ (y \ x) <= x \ (y \ x) by BCIALG_1:5; then y \ (y \ x) <= x \ (y \ x) by A1, Th28; then A4: (y \ (y \ x)) \ (x \ (y \ x)) = 0. X by BCIALG_1:def_11; (x \ (x \ (y \ (y \ x)))) \ (y \ (y \ x)) = (x \ (y \ (y \ x))) \ (x \ (y \ (y \ x))) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ x)) = 0. X by A4, BCIALG_1:3; then x \ (x \ (y \ (y \ x))) <= x \ (y \ x) by BCIALG_1:def_11; then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (y \ x)) \ (x \ (y \ (y \ x))) by BCIALG_1:5; then (x \ (x \ (y \ (y \ x)))) \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by BCIALG_1:7; then x \ (x \ (y \ (y \ x))) <= (x \ (x \ (y \ (y \ x)))) \ (y \ x) by A1, Th28; then A5: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) = 0. X by BCIALG_1:def_11; (y \ (y \ x)) \ y = (y \ y) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then y \ (y \ x) <= y by BCIALG_1:def_11; then x \ y <= x \ (y \ (y \ x)) by BCIALG_1:5; then x \ (x \ (y \ (y \ x))) <= x \ (x \ y) by BCIALG_1:5; then (x \ (x \ (y \ (y \ x)))) \ (y \ x) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:5; then ((x \ (x \ (y \ (y \ x)))) \ (y \ x)) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by BCIALG_1:def_11; then (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by A5, BCIALG_1:3; hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; ::_thesis: verum end; assume A6: for x, y being Element of X holds (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y A7: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8 .= (x \ y) \ (0. X) by BCIALG_1:def_5 .= x \ y by BCIALG_1:2 ; ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7 .= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def_5 .= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def_8 .= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; hence x \ y = (x \ y) \ y by A6, A7; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum end; theorem :: BCIALG_3:30 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) ::_thesis: ( ( for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ (x \ (x \ y)) A2: ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) = ((x \ y) \ ((x \ x) \ y)) \ (x \ (x \ y)) by BCIALG_1:7 .= ((x \ y) \ (y `)) \ (x \ (x \ y)) by BCIALG_1:def_5 .= ((x \ y) \ (0. X)) \ (x \ (x \ y)) by BCIALG_1:def_8 .= (x \ y) \ (x \ (x \ y)) by BCIALG_1:2 ; (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8 .= (x \ y) \ (0. X) by BCIALG_1:def_5 .= x \ y by BCIALG_1:2 ; hence x \ y = (x \ y) \ (x \ (x \ y)) by A1, A2, Th29; ::_thesis: verum end; assume A3: for x, y being Element of X holds x \ y = (x \ y) \ (x \ (x \ y)) ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y (x \ y) \ (x \ (x \ y)) = (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; hence x \ y = (x \ y) \ y by A3; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum end; theorem :: BCIALG_3:31 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z let x, y, z be Element of X; ::_thesis: (x \ z) \ (y \ z) <= (x \ y) \ z ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = ((x \ z) \ (y \ z)) \ ((x \ z) \ (y \ z)) by A1, Def11 .= 0. X by BCIALG_1:def_5 ; hence (x \ z) \ (y \ z) <= (x \ y) \ z by BCIALG_1:def_11; ::_thesis: verum end; assume A2: for x, y, z being Element of X holds (x \ z) \ (y \ z) <= (x \ y) \ z ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ (y \ z) proof let x, y, z be Element of X; ::_thesis: (x \ y) \ z = (x \ z) \ (y \ z) (y \ z) \ y = (y \ y) \ z by BCIALG_1:7 .= z ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then y \ z <= y by BCIALG_1:def_11; then x \ y <= x \ (y \ z) by BCIALG_1:5; then (x \ y) \ z <= (x \ (y \ z)) \ z by BCIALG_1:5; then ((x \ y) \ z) \ ((x \ (y \ z)) \ z) = 0. X by BCIALG_1:def_11; then A3: ((x \ y) \ z) \ ((x \ z) \ (y \ z)) = 0. X by BCIALG_1:7; (x \ z) \ (y \ z) <= (x \ y) \ z by A2; then ((x \ z) \ (y \ z)) \ ((x \ y) \ z) = 0. X by BCIALG_1:def_11; hence (x \ y) \ z = (x \ z) \ (y \ z) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Def11; ::_thesis: verum end; theorem :: BCIALG_3:32 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ y <= (x \ y) \ y ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ y <= (x \ y) \ y ) ::_thesis: ( ( for x, y being Element of X holds x \ y <= (x \ y) \ y ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ y <= (x \ y) \ y let x, y be Element of X; ::_thesis: x \ y <= (x \ y) \ y (x \ y) \ ((x \ y) \ y) = ((x \ y) \ y) \ ((x \ y) \ y) by A1, Th28 .= 0. X by BCIALG_1:def_5 ; hence x \ y <= (x \ y) \ y by BCIALG_1:def_11; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ y <= (x \ y) \ y ; ::_thesis: X is BCK-positive-implicative BCK-algebra for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y x \ y <= (x \ y) \ y by A2; then A3: (x \ y) \ ((x \ y) \ y) = 0. X by BCIALG_1:def_11; ((x \ y) \ y) \ (x \ y) = ((x \ y) \ (x \ y)) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ y = (x \ y) \ y by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Th28; ::_thesis: verum end; theorem :: BCIALG_3:33 for X being BCK-algebra holds ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-positive-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) thus ( X is BCK-positive-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ) implies X is BCK-positive-implicative BCK-algebra ) proof assume A1: X is BCK-positive-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) let x, y be Element of X; ::_thesis: x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = (x \ (x \ (y \ (y \ x)))) \ (x \ (x \ (y \ (y \ x)))) by A1, Th29 .= 0. X by BCIALG_1:def_5 ; hence x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) by BCIALG_1:def_11; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) ; ::_thesis: X is BCK-positive-implicative BCK-algebra 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))) x \ (x \ (y \ (y \ x))) <= (x \ (x \ y)) \ (y \ x) by A2; then A3: (x \ (x \ (y \ (y \ x)))) \ ((x \ (x \ y)) \ (y \ x)) = 0. X by BCIALG_1:def_11; ((x \ (x \ y)) \ (y \ x)) \ (x \ (x \ (y \ (y \ x)))) = 0. X by BCIALG_1:10; hence (x \ (x \ y)) \ (y \ x) = x \ (x \ (y \ (y \ x))) by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-positive-implicative BCK-algebra by Th29; ::_thesis: verum end; theorem Th34: :: BCIALG_3:34 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) ) thus ( X is BCK-implicative BCK-algebra implies ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) ) ::_thesis: ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) A2: for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) <= y \ (y \ x) (x \ (x \ y)) \ y = (x \ y) \ (x \ y) by BCIALG_1:7 .= 0. X by BCIALG_1:def_5 ; then x \ (x \ y) <= y by BCIALG_1:def_11; then (x \ (x \ y)) \ (y \ x) <= y \ (y \ x) by BCIALG_1:5; then (x \ (y \ x)) \ (x \ y) <= y \ (y \ x) by BCIALG_1:7; hence x \ (x \ y) <= y \ (y \ x) by A1, Def12; ::_thesis: verum end; for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y (x \ y) \ (y \ (x \ y)) = x \ y by A1, Def12; hence x \ y = (x \ y) \ y by A1, Def12; ::_thesis: verum end; hence ( X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra ) by A2, Th1, Th28; ::_thesis: verum end; assume that A3: X is commutative BCK-algebra and A4: X is BCK-positive-implicative BCK-algebra ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x x \ (x \ (x \ (y \ x))) = x \ (y \ x) by BCIALG_1:8; then A5: x \ (y \ x) = x \ ((y \ x) \ ((y \ x) \ x)) by A3, Def1; (y \ x) \ ((y \ x) \ x) = (y \ x) \ (y \ x) by A4, Th28 .= 0. X by BCIALG_1:def_5 ; hence x \ (y \ x) = x by A5, BCIALG_1:2; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum end; theorem Th35: :: BCIALG_3:35 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) X is commutative BCK-algebra by A1, Th34; then (x \ (x \ y)) \ (x \ y) = (y \ (y \ x)) \ (x \ y) by Def1 .= (y \ (x \ y)) \ (y \ x) by BCIALG_1:7 ; hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, Def12; ::_thesis: verum end; assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X holds (x \ y) \ y = x \ y proof let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y A3: (x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; A4: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; (x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ ((x \ y) \ x) by A2; hence (x \ y) \ y = x \ y by A3, A4, BCIALG_1:2; ::_thesis: verum end; then A5: X is BCK-positive-implicative BCK-algebra by Th28; for x, y being Element of X st x <= y holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) ) assume x <= y ; ::_thesis: x = y \ (y \ x) then A6: x \ y = 0. X by BCIALG_1:def_11; then y \ (y \ x) = (x \ (x \ y)) \ (0. X) by A2 .= x \ (0. X) by A6, BCIALG_1:2 ; hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum end; then X is commutative BCK-algebra by Th5; hence X is BCK-implicative BCK-algebra by A5, Th34; ::_thesis: verum end; theorem :: BCIALG_3:36 for X being non empty BCIStr_0 holds ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) proof let X be non empty BCIStr_0 ; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) ::_thesis: ( ( for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) then A2: X is commutative BCK-algebra by Th34; let x, y, z be Element of X; ::_thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) A3: x \ ((0. X) \ y) = x \ (y `) .= x \ (0. X) by A1, BCIALG_1:def_8 .= x by A1, BCIALG_1:2 ; ((y \ z) \ (y \ x)) \ (x \ y) = ((y \ z) \ (x \ y)) \ (y \ x) by A1, BCIALG_1:7 .= ((y \ (x \ y)) \ z) \ (y \ x) by A1, BCIALG_1:7 .= (y \ z) \ (y \ x) by A1, Def12 .= (y \ (y \ x)) \ z by A1, BCIALG_1:7 .= (x \ (x \ y)) \ z by A2, Def1 .= (x \ z) \ (x \ y) by A1, BCIALG_1:7 ; hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) by A3; ::_thesis: verum end; assume A4: for x, y, z being Element of X holds ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ; ::_thesis: X is BCK-implicative BCK-algebra A5: for x, y being Element of X holds x \ (0. X) = x proof let x, y be Element of X; ::_thesis: x \ (0. X) = x (0. X) \ ((0. X) \ (0. X)) = 0. X by A4; hence x \ (0. X) = x by A4; ::_thesis: verum end; A6: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds x = y proof let x, y be Element of X; ::_thesis: ( x \ y = 0. X & y \ x = 0. X implies x = y ) assume ( x \ y = 0. X & y \ x = 0. X ) ; ::_thesis: x = y then (x \ (0. X)) \ (0. X) = ((y \ (0. X)) \ (0. X)) \ (0. X) by A4 .= (y \ (0. X)) \ (0. X) by A5 ; then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5 .= y \ (0. X) by A5 ; hence x = y \ (0. X) by A5 .= y by A5 ; ::_thesis: verum end; A7: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = (y \ (y \ x)) \ (x \ y) x \ (x \ y) = (x \ (0. X)) \ (x \ y) by A5 .= ((y \ (0. X)) \ (y \ x)) \ (x \ y) by A4 ; hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A5; ::_thesis: verum end; A8: for y being Element of X holds y \ y = 0. X proof let y be Element of X; ::_thesis: y \ y = 0. X (0. X) \ ((0. X) \ y) = (y \ (y \ (0. X))) \ ((0. X) \ y) by A7 .= (y \ y) \ ((0. X) \ y) by A5 .= y \ y by A4 ; hence y \ y = 0. X by A4; ::_thesis: verum end; A9: for x being Element of X holds (0. X) \ x = 0. X proof let x be Element of X; ::_thesis: (0. X) \ x = 0. X ((0. X) \ x) \ ((0. X) \ x) = (0. X) \ x by A4; hence (0. X) \ x = 0. X by A8; ::_thesis: verum end; A10: for x, y being Element of X holds (x \ y) \ x = 0. X proof let x, y be Element of X; ::_thesis: (x \ y) \ x = 0. X (x \ y) \ x = (x \ y) \ (x \ (0. X)) by A5 .= (((0. X) \ y) \ ((0. X) \ x)) \ (x \ (0. X)) by A4 .= ((0. X) \ ((0. X) \ x)) \ (x \ (0. X)) by A9 .= (0. X) \ (x \ (0. X)) by A9 ; hence (x \ y) \ x = 0. X by A9; ::_thesis: verum end; A11: for x, y, z being Element of X holds ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X proof let x, y, z be Element of X; ::_thesis: ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X (((y \ z) \ (y \ x)) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A10; hence ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X by A4; ::_thesis: verum end; A12: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ (y \ x) proof let x, y, z be Element of X; ::_thesis: (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ( ((y \ z) \ (y \ x)) \ ((x \ z) \ (x \ y)) = 0. X & ((x \ z) \ (x \ y)) \ ((y \ z) \ (y \ x)) = 0. X ) by A11; hence (x \ z) \ (x \ y) = (y \ z) \ (y \ x) by A6; ::_thesis: verum end; then A13: X is commutative BCK-algebra by A4, Th6; for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) x \ (x \ y) = y \ (y \ x) by A13, Def1; hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A7; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by A4, A12, Th6, Th35; ::_thesis: verum end; Lm1: for X being bounded BCK-algebra st X is BCK-implicative holds for a being Element of X st a is being_greatest holds for x being Element of X holds a \ (a \ x) = x proof let X be bounded BCK-algebra; ::_thesis: ( X is BCK-implicative implies for a being Element of X st a is being_greatest holds for x being Element of X holds a \ (a \ x) = x ) assume X is BCK-implicative ; ::_thesis: for a being Element of X st a is being_greatest holds for x being Element of X holds a \ (a \ x) = x then A1: X is commutative BCK-algebra by Th34; let a be Element of X; ::_thesis: ( a is being_greatest implies for x being Element of X holds a \ (a \ x) = x ) assume A2: a is being_greatest ; ::_thesis: for x being Element of X holds a \ (a \ x) = x let x be Element of X; ::_thesis: a \ (a \ x) = x a \ (a \ x) = x \ (x \ a) by A1, Def1 .= x \ (0. X) by A2, Def2 ; hence a \ (a \ x) = x by BCIALG_1:2; ::_thesis: verum end; theorem Th37: :: BCIALG_3:37 for X being bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) proof let X be bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff ( X is involutory & X is BCK-positive-implicative ) ) thus ( X is BCK-implicative implies ( X is involutory & X is BCK-positive-implicative ) ) ::_thesis: ( X is involutory & X is BCK-positive-implicative implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: ( X is involutory & X is BCK-positive-implicative ) then for a being Element of X st a is being_greatest holds for x being Element of X holds a \ (a \ x) = x by Lm1; hence ( X is involutory & X is BCK-positive-implicative ) by A2, Def7, Th34; ::_thesis: verum end; assume that A3: X is involutory and A4: X is BCK-positive-implicative ; ::_thesis: X is BCK-implicative for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x y \ a = 0. X by A1, Def2; then y <= a by BCIALG_1:def_11; then A5: y \ x <= a \ x by BCIALG_1:5; x \ (a \ x) = (a \ (a \ x)) \ (a \ x) by A1, A3, Def7 .= a \ (a \ x) by A4, Th28 .= x by A1, A3, Def7 ; then x <= x \ (y \ x) by A5, BCIALG_1:5; then A6: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_11; (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (y \ x) = x by A6, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-implicative by Def12; ::_thesis: verum end; theorem :: BCIALG_3:38 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X let x, y be Element of X; ::_thesis: x \ (x \ (y \ x)) = 0. X x \ (x \ (y \ x)) = x \ x by A1, Def12; hence x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_5; ::_thesis: verum end; assume A2: for x, y being Element of X holds x \ (x \ (y \ x)) = 0. X ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x A3: (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; x \ (x \ (y \ x)) = 0. X by A2; hence x \ (y \ x) = x by A3, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum end; theorem :: BCIALG_3:39 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) ::_thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) X is commutative BCK-algebra by A1, Th34; then y \ (y \ (x \ (x \ y))) = y \ (y \ (y \ (y \ x))) by Def1 .= y \ (y \ x) by BCIALG_1:8 ; hence (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Th35; ::_thesis: verum end; assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ; ::_thesis: X is BCK-implicative BCK-algebra A3: for x, y being Element of X holds (x \ y) \ y = x \ y proof let x, y be Element of X; ::_thesis: (x \ y) \ y = x \ y A4: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8 .= (x \ y) \ (0. X) by BCIALG_1:def_5 .= x \ y by BCIALG_1:2 ; (x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; hence (x \ y) \ y = x \ y by A2, A4; ::_thesis: verum end; for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y))) x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A3; hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2; ::_thesis: verum end; then A5: X is commutative BCK-algebra by Th4; for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x) (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2 .= y \ (y \ (y \ (y \ x))) by A5, Def1 ; hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by BCIALG_1:8; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by Th35; ::_thesis: verum end; theorem Th40: :: BCIALG_3:40 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) then A2: X is commutative BCK-algebra by Th34; let x, y, z be Element of X; ::_thesis: (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) A3: (x \ z) \ (x \ y) = (x \ (x \ y)) \ z by BCIALG_1:7 .= (y \ (y \ x)) \ z by A2, Def1 ; X is BCK-positive-implicative BCK-algebra by A1, Th34; hence (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) by A3, Def11; ::_thesis: verum end; assume A4: for x, y, z being Element of X holds (x \ z) \ (x \ y) = (y \ z) \ ((y \ x) \ z) ; ::_thesis: X is BCK-implicative BCK-algebra A5: for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = y \ (y \ x) (x \ (0. X)) \ (x \ y) = (y \ (0. X)) \ ((y \ x) \ (0. X)) by A4; then (x \ (0. X)) \ (x \ y) = y \ ((y \ x) \ (0. X)) by BCIALG_1:2; then (x \ (0. X)) \ (x \ y) = y \ (y \ x) by BCIALG_1:2; hence x \ (x \ y) = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum end; for x, y being Element of X holds (y \ (y \ x)) \ (y \ x) = x \ (x \ y) proof let x, y be Element of X; ::_thesis: (y \ (y \ x)) \ (y \ x) = x \ (x \ y) (x \ (y \ x)) \ (x \ y) = (y \ (y \ x)) \ ((y \ x) \ (y \ x)) by A4; then (x \ (y \ x)) \ (x \ y) = (y \ (y \ x)) \ (0. X) by BCIALG_1:def_5; then (x \ (y \ x)) \ (x \ y) = y \ (y \ x) by BCIALG_1:2; then (x \ (x \ y)) \ (y \ x) = y \ (y \ x) by BCIALG_1:7; then (y \ (y \ x)) \ (y \ x) = y \ (y \ x) by A5; hence (y \ (y \ x)) \ (y \ x) = x \ (x \ y) by A5; ::_thesis: verum end; then for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ; hence X is BCK-implicative BCK-algebra by Th35; ::_thesis: verum end; theorem :: BCIALG_3:41 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) thus ( X is BCK-implicative BCK-algebra implies for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) ::_thesis: ( ( for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) then A2: X is BCK-positive-implicative BCK-algebra by Th34; for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) proof let x, y, z be Element of X; ::_thesis: x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) (x \ (0. X)) \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by A1, Th40; then x \ (x \ (y \ z)) = ((y \ z) \ (0. X)) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2 .= (y \ z) \ (((y \ z) \ x) \ (0. X)) by BCIALG_1:2 ; then x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ x) by BCIALG_1:2 .= (y \ z) \ ((y \ x) \ z) by BCIALG_1:7 ; hence x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) by A2, Def11; ::_thesis: verum end; hence for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ; ::_thesis: verum end; assume A3: for x, y, z being Element of X holds x \ (x \ (y \ z)) = (y \ z) \ ((y \ z) \ (x \ z)) ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (x \ x)) by A3; then x \ (x \ (y \ x)) = (y \ x) \ ((y \ x) \ (0. X)) by BCIALG_1:def_5; then x \ (x \ (y \ x)) = (y \ x) \ (y \ x) by BCIALG_1:2; then A4: x \ (x \ (y \ x)) = 0. X by BCIALG_1:def_5; (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (y \ x) = x by A4, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-implicative BCK-algebra by Def12; ::_thesis: verum end; theorem :: BCIALG_3:42 for X being BCK-algebra holds ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) proof let X be BCK-algebra; ::_thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) ::_thesis: ( ( for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ) implies X is BCK-implicative BCK-algebra ) proof assume A1: X is BCK-implicative BCK-algebra ; ::_thesis: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) then A2: X is commutative BCK-algebra by Th34; for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) proof let x, y be Element of X; ::_thesis: x \ (x \ y) = (y \ (y \ x)) \ (x \ y) (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A1, Th35; then (y \ (y \ x)) \ (x \ y) = y \ (y \ x) by A2, Def1; hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A2, Def1; ::_thesis: verum end; hence for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ; ::_thesis: verum end; assume A3: for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ; ::_thesis: X is BCK-implicative BCK-algebra for x, y being Element of X st x <= y holds x = y \ (y \ x) proof let x, y be Element of X; ::_thesis: ( x <= y implies x = y \ (y \ x) ) assume x <= y ; ::_thesis: x = y \ (y \ x) then x \ y = 0. X by BCIALG_1:def_11; then x \ (0. X) = (y \ (y \ x)) \ (0. X) by A3; then x \ (0. X) = y \ (y \ x) by BCIALG_1:2; hence x = y \ (y \ x) by BCIALG_1:2; ::_thesis: verum end; then A4: X is commutative BCK-algebra by Th5; for x, y being Element of X holds x \ y = (x \ y) \ y proof let x, y be Element of X; ::_thesis: x \ y = (x \ y) \ y A5: (x \ y) \ x = (x \ x) \ y by BCIALG_1:7 .= y ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; x \ (x \ (x \ y)) = ((x \ y) \ ((x \ y) \ x)) \ (x \ (x \ y)) by A3; then x \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by A5, BCIALG_1:2 .= (x \ (x \ (x \ y))) \ y by BCIALG_1:7 .= (x \ y) \ y by BCIALG_1:8 ; hence x \ y = (x \ y) \ y by BCIALG_1:8; ::_thesis: verum end; then X is BCK-positive-implicative BCK-algebra by Th28; hence X is BCK-implicative BCK-algebra by A4, Th34; ::_thesis: verum end; theorem Th43: :: BCIALG_3:43 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) thus ( X is BCK-implicative implies for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) ::_thesis: ( ( for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X (a \ x) \ ((a \ x) \ x) = x \ (x \ (a \ x)) by Def1 .= x \ x by A2, Def12 ; hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def_5; ::_thesis: verum end; assume A3: for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X ; ::_thesis: X is BCK-implicative for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x (a \ x) \ ((a \ x) \ x) = 0. X by A3; then A4: x \ (x \ (a \ x)) = 0. X by Def1; y \ a = 0. X by A1, Def2; then y <= a by BCIALG_1:def_11; then y \ x <= a \ x by BCIALG_1:5; then A5: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5; (x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7 .= (a \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (a \ x) = x by A4, BCIALG_1:def_7; then A6: x \ (x \ (y \ x)) = 0. X by A5, BCIALG_1:def_11; (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (y \ x) = x by A6, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-implicative by Def12; ::_thesis: verum end; theorem :: BCIALG_3:44 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds x \ (a \ x) = x ) thus ( X is BCK-implicative implies for x being Element of X holds x \ (a \ x) = x ) ::_thesis: ( ( for x being Element of X holds x \ (a \ x) = x ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds x \ (a \ x) = x for x being Element of X holds x \ (a \ x) = x proof let x be Element of X; ::_thesis: x \ (a \ x) = x (a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43; then A3: x \ (x \ (a \ x)) = 0. X by Def1; (x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7 .= (a \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (a \ x) = x by A3, BCIALG_1:def_7; ::_thesis: verum end; hence for x being Element of X holds x \ (a \ x) = x ; ::_thesis: verum end; assume A4: for x being Element of X holds x \ (a \ x) = x ; ::_thesis: X is BCK-implicative for x, y being Element of X holds x \ (y \ x) = x proof let x, y be Element of X; ::_thesis: x \ (y \ x) = x A5: (x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7 .= (a \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; y \ a = 0. X by A1, Def2; then y <= a by BCIALG_1:def_11; then y \ x <= a \ x by BCIALG_1:5; then A6: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5; x \ (x \ (a \ x)) = x \ x by A4 .= 0. X by BCIALG_1:def_5 ; then x \ (a \ x) = x by A5, BCIALG_1:def_7; then A7: x \ (x \ (y \ x)) = 0. X by A6, BCIALG_1:def_11; (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (y \ x) = x by A7, BCIALG_1:def_7; ::_thesis: verum end; hence X is BCK-implicative by Def12; ::_thesis: verum end; theorem :: BCIALG_3:45 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x being Element of X holds (a \ x) \ x = a \ x ) thus ( X is BCK-implicative implies for x being Element of X holds (a \ x) \ x = a \ x ) ::_thesis: ( ( for x being Element of X holds (a \ x) \ x = a \ x ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x being Element of X holds (a \ x) \ x = a \ x let x be Element of X; ::_thesis: (a \ x) \ x = a \ x A3: ((a \ x) \ x) \ (a \ x) = ((a \ x) \ (a \ x)) \ x by BCIALG_1:7 .= x ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; (a \ x) \ ((a \ x) \ x) = 0. X by A1, A2, Th43; hence (a \ x) \ x = a \ x by A3, BCIALG_1:def_7; ::_thesis: verum end; assume A4: for x being Element of X holds (a \ x) \ x = a \ x ; ::_thesis: X is BCK-implicative let x, y be Element of X; :: according to BCIALG_3:def_12 ::_thesis: x \ (y \ x) = x (a \ x) \ ((a \ x) \ x) = (a \ x) \ (a \ x) by A4 .= 0. X by BCIALG_1:def_5 ; then A5: x \ (x \ (a \ x)) = 0. X by Def1; y \ a = 0. X by A1, Def2; then y <= a by BCIALG_1:def_11; then y \ x <= a \ x by BCIALG_1:5; then A6: x \ (a \ x) <= x \ (y \ x) by BCIALG_1:5; (x \ (a \ x)) \ x = (x \ x) \ (a \ x) by BCIALG_1:7 .= (a \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (a \ x) = x by A5, BCIALG_1:def_7; then A7: x \ (x \ (y \ x)) = 0. X by A6, BCIALG_1:def_11; (x \ (y \ x)) \ x = (x \ x) \ (y \ x) by BCIALG_1:7 .= (y \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; hence x \ (y \ x) = x by A7, BCIALG_1:def_7; ::_thesis: verum end; theorem Th46: :: BCIALG_3:46 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) thus ( X is BCK-implicative implies for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) ::_thesis: ( ( for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y let x, y be Element of X; ::_thesis: (a \ y) \ ((a \ y) \ x) = x \ y X is involutory by A1, A2, Th37; then A3: x \ (a \ y) = y \ (a \ x) by A1, Th23; A4: (a \ y) \ ((a \ y) \ x) = x \ (x \ (a \ y)) by Def1; (y \ (a \ x)) \ y = (y \ y) \ (a \ x) by BCIALG_1:7 .= (a \ x) ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then x \ (a \ y) <= y by A3, BCIALG_1:def_11; then x \ y <= (a \ y) \ ((a \ y) \ x) by A4, BCIALG_1:5; then A5: (x \ y) \ ((a \ y) \ ((a \ y) \ x)) = 0. X by BCIALG_1:def_11; X is BCK-positive-implicative BCK-algebra by A2, Th34; then a \ y = (a \ y) \ y by Th28; then ((a \ y) \ ((a \ y) \ x)) \ (x \ y) = 0. X by BCIALG_1:1; hence (a \ y) \ ((a \ y) \ x) = x \ y by A5, BCIALG_1:def_7; ::_thesis: verum end; assume A6: for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y ; ::_thesis: X is BCK-implicative for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X proof let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X (a \ x) \ ((a \ x) \ x) = x \ x by A6; hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def_5; ::_thesis: verum end; hence X is BCK-implicative by A1, Th43; ::_thesis: verum end; theorem Th47: :: BCIALG_3:47 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) thus ( X is BCK-implicative implies for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) ::_thesis: ( ( for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) let x, y be Element of X; ::_thesis: y \ (y \ x) = x \ (a \ y) y \ (y \ x) = x \ (x \ y) by Def1 .= x \ ((a \ y) \ ((a \ y) \ x)) by A1, A2, Th46 .= x \ (x \ (x \ (a \ y))) by Def1 ; hence y \ (y \ x) = x \ (a \ y) by BCIALG_1:8; ::_thesis: verum end; assume A3: for x, y being Element of X holds y \ (y \ x) = x \ (a \ y) ; ::_thesis: X is BCK-implicative for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y proof let x, y be Element of X; ::_thesis: (a \ y) \ ((a \ y) \ x) = x \ y (a \ y) \ ((a \ y) \ x) = x \ (a \ (a \ y)) by A3 .= x \ (y \ (y \ a)) by Def1 .= x \ (y \ (0. X)) by A1, Def2 ; hence (a \ y) \ ((a \ y) \ x) = x \ y by BCIALG_1:2; ::_thesis: verum end; hence X is BCK-implicative by A1, Th46; ::_thesis: verum end; theorem :: BCIALG_3:48 for X being commutative bounded BCK-algebra for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) proof let X be commutative bounded BCK-algebra; ::_thesis: for a being Element of X st a is being_greatest holds ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) let a be Element of X; ::_thesis: ( a is being_greatest implies ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) ) assume A1: a is being_greatest ; ::_thesis: ( X is BCK-implicative iff for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) thus ( X is BCK-implicative implies for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) ::_thesis: ( ( for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ) implies X is BCK-implicative ) proof assume A2: X is BCK-implicative ; ::_thesis: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) let x, y, z be Element of X; ::_thesis: (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) X is BCK-positive-implicative BCK-algebra by A2, Th34; then A3: ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ y) \ z) = ((x \ (y \ z)) \ (x \ (x \ z))) \ ((x \ z) \ (y \ z)) by Def11 .= 0. X by BCIALG_1:1 ; ((x \ y) \ z) \ (x \ y) = ((x \ y) \ (x \ y)) \ z by BCIALG_1:7 .= z ` by BCIALG_1:def_5 .= 0. X by BCIALG_1:def_8 ; then A4: ((x \ (y \ z)) \ (x \ (x \ z))) \ (x \ y) = 0. X by A3, BCIALG_1:3; ((x \ (y \ z)) \ (x \ y)) \ (x \ (a \ z)) = ((x \ (y \ z)) \ (x \ y)) \ (z \ (z \ x)) by A1, A2, Th47 .= ((x \ (y \ z)) \ (x \ y)) \ (x \ (x \ z)) by Def1 .= 0. X by A4, BCIALG_1:7 ; hence (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) by BCIALG_1:def_11; ::_thesis: verum end; assume A5: for x, y, z being Element of X holds (x \ (y \ z)) \ (x \ y) <= x \ (a \ z) ; ::_thesis: X is BCK-implicative for x being Element of X holds (a \ x) \ ((a \ x) \ x) = 0. X proof let x be Element of X; ::_thesis: (a \ x) \ ((a \ x) \ x) = 0. X (x \ (x \ x)) \ (x \ x) <= x \ (a \ x) by A5; then (x \ (0. X)) \ (x \ x) <= x \ (a \ x) by BCIALG_1:def_5; then x \ (x \ x) <= x \ (a \ x) by BCIALG_1:2; then x \ (0. X) <= x \ (a \ x) by BCIALG_1:def_5; then x <= x \ (a \ x) by BCIALG_1:2; then x \ (x \ (a \ x)) = 0. X by BCIALG_1:def_11; hence (a \ x) \ ((a \ x) \ x) = 0. X by Def1; ::_thesis: verum end; hence X is BCK-implicative by A1, Th43; ::_thesis: verum end;