:: Several Classes of {BCK}-algebras and Their Properties :: by Tao Sun , Dahai Hu and Xiquan Liang :: :: Received September 19, 2007 :: Copyright (c) 2007-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, BCIALG_1, BINOP_1, SUBSET_1, XXREAL_0, SUPINF_2, XXREAL_2, CARD_FIL, BCIALG_3; notations XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1; constructors BCIALG_1; registrations STRUCT_0, BCIALG_1; requirements SUBSET; equalities BCIALG_1; expansions BCIALG_1; theorems BCIALG_1, STRUCT_0; begin :: The Basics of General Theory of commutative BCK-algebra definition let IT be non empty BCIStr_0; attr IT is commutative means :Def1: for x,y being Element of IT holds x\(x\y ) = y\(y\x); end; registration cluster BCI-EXAMPLE -> commutative; coherence by STRUCT_0:def 10; end; registration cluster commutative for BCK-algebra; existence proof take BCI-EXAMPLE; thus thesis; end; end; reserve X for BCK-algebra; reserve x,y for Element of X; reserve IT for non empty Subset of X; theorem Th1: X is commutative BCK-algebra iff for x,y being Element of X holds x\(x\y) <= y\(y\x) proof thus X is commutative BCK-algebra implies for x,y being Element of X holds x \(x\y) <= y\(y\x) proof assume A1: X is commutative BCK-algebra; let x,y be Element of 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 thesis; end; assume A2: for x,y being Element of X holds x\(x\y) <= y\(y\x); for x,y being Element of X holds x\(x\y) = y\(y\x) proof let x,y; y\(y\x) <= x\(x\y) by A2; then A3: (y\(y\x))\(x\(x\y)) = 0.X; x\(x\y) <= y\(y\x) by A2; then (x\(x\y))\(y\(y\x)) = 0.X; hence thesis by A3,BCIALG_1:def 7; end; hence thesis by Def1; end; theorem Th2: for X being BCK-algebra holds for x,y being Element of X holds x\ (x\y) <= y & x\(x\y) <= x proof let X be BCK-algebra; let x,y be Element of 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,2; hence thesis; end; theorem Th3: X is commutative BCK-algebra iff for x,y being Element of X holds x\y = x\(y\(y\x)) proof thus X is commutative BCK-algebra implies for x,y being Element of X holds x \y = x\(y\(y\x)) proof assume A1: X is commutative BCK-algebra; let x,y be Element of X; x\y = x\(x\(x\y)) by BCIALG_1:8 .= x\(y\(y\x)) by A1,Def1; hence thesis; end; assume A2: for x,y being Element of X holds x\y = x\(y\(y\x)); for x,y being Element of X holds x\(x\y) <= y\(y\x) proof let x,y; x\(x\(y\(y\x))) <= y\(y\x) by Th2; hence thesis by A2; end; hence thesis by Th1; end; theorem Th4: X is commutative BCK-algebra iff for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y))) proof thus X is commutative BCK-algebra implies for x,y being Element of X holds x \(x\y) = y\(y\(x\(x\y))) proof assume A1: X is commutative BCK-algebra; let x,y be Element of X; y\(y\x) = y\(y\(x\(x\y))) by A1,Th3; hence thesis by A1,Def1; end; assume A2: for x,y being Element of X holds x\(x\y) = y\(y\(x\(x\y))); for x,y being Element of X holds x\(x\y) <= y\(y\x) proof let x,y; 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 thesis by A3,BCIALG_1:5; end; hence thesis by Th1; end; theorem Th5: X is commutative BCK-algebra iff for x,y being Element of X st x <= y holds x= y\(y\x) proof thus X is commutative BCK-algebra implies for x,y being Element of X st x<= y holds x= y\(y\x) proof assume A1: X is commutative BCK-algebra; let x,y be Element of X; assume x<= y; then x\y = 0.X; then y\(y\x) = x\0.X by A1,Def1 .=x by BCIALG_1:2; hence thesis; end; assume A2: for x,y being Element of X st x<= y holds x= y\(y\x); for x,y being Element of X holds x\(x\y) <= y\(y\x) proof let x,y be Element of 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; 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; then (x\(x\y))= y\(y\(x\(x\y))) by A2; hence thesis by A3,BCIALG_1:5; end; hence thesis by Th1; end; theorem Th6: 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; 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) proof assume A1: X is commutative BCK-algebra; let x,y,z be Element of 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 thesis by A1,A2,BCIALG_1:2; 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); A4: for x,y being Element of X holds x\(x\y) = y\(y\x) proof let x,y be Element of 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 thesis; end; A5: for x,y being Element of X holds x\0.X = x proof let x,y be Element of X; 0.X\(0.X\0.X) = 0.X by A3; hence thesis by A3; end; for x,y being Element of X holds (x\y=0.X & y\x=0.X implies x = y) proof let x,y be Element of X; assume x\y=0.X & y\x=0.X; 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; end; then A6: X is being_BCI-4; A7: for x being Element of X holds x\x = 0.X proof let x be Element of 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 thesis; end; A8: for x being Element of X holds 0.X\x = 0.X proof let x be Element of X; 0.X = (0.X\x)\(0.X\x) by A7 .= 0.X\x by A3; hence thesis; 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; ((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 thesis; end; A10: for x,y being Element of X holds (x\(x\y))\y = 0.X proof let x,y be Element of 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 thesis; end; A11: X is being_I by A7; for x being Element of X holds x`=0.X by A8; hence thesis by A4,A9,A10,A11,A6,Def1,BCIALG_1:1,def 8; end; theorem X is commutative BCK-algebra implies for x,y being Element of X st x\y =x holds y\x=y proof assume A1: X is commutative BCK-algebra; let x,y be Element of X; assume x\y=x; 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 thesis; end; theorem Th8: X is commutative BCK-algebra implies for x,y,a being Element of X st y <= a holds (a\x)\(a\y) = y\x proof assume A1: X is commutative BCK-algebra; let x,y,a be Element of X; assume y <= a; then A2: y\a = 0.X; (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 thesis; end; theorem X is commutative BCK-algebra implies for x,y being Element of X holds (x\y=x iff y\(y\x)=0.X) proof assume A1: X is commutative BCK-algebra; A2: for x,y being Element of X holds (y\(y\x)=0.X implies x\y=x) proof let x,y be Element of X; assume A3: y\(y\x)=0.X; x\y = x\(x\(x\y)) by BCIALG_1:8 .= x\0.X by A1,A3,Def1 .= x by BCIALG_1:2; hence thesis; end; for x,y being Element of X holds (x\y=x implies y\(y\x)=0.X) proof let x,y be Element of X; assume x\y=x; then y\(y\x) = x\x by A1,Def1 .= 0.X by BCIALG_1:def 5; hence thesis; end; hence thesis by A2; end; theorem 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 proof assume A1: X is commutative BCK-algebra; let x,y be Element of X; 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 thesis by A2; end; theorem X is commutative BCK-algebra implies 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; attr a is being_greatest means for x being Element of X holds x\a=0.X; attr a is being_positive means 0.X\a=0.X; end; begin :: Several Classes of BCI-algebra---commutative BCI-algebra definition let IT be BCI-algebra; attr IT is BCI-commutative means :Def4: for x,y being Element of IT st x\y= 0.IT holds x = y\(y\x); attr IT is BCI-weakly-commutative means :Def5: for x,y being Element of IT holds (x\(x\y))\(0.IT\(x\y)) = y\(y\x); end; registration cluster BCI-EXAMPLE -> BCI-commutative BCI-weakly-commutative; coherence by STRUCT_0:def 10; end; registration cluster BCI-commutative BCI-weakly-commutative for BCI-algebra; existence proof take BCI-EXAMPLE; thus thesis; end; end; theorem for X being BCI-algebra holds ((ex a be Element of X st a is being_greatest) implies X is BCK-algebra) proof let X be BCI-algebra; given a being Element of X such that A1: a is being_greatest; for x being Element of X holds x`=0.X proof let x be Element of X; x\a=0.X by A1; then x` = (x\x)\a by BCIALG_1:7 .= 0.X by A1; hence thesis; end; hence thesis by BCIALG_1:def 8; end; theorem for X being BCI-algebra holds (X is p-Semisimple implies X is BCI-commutative & X is BCI-weakly-commutative ) proof let X being BCI-algebra; assume A1: X is p-Semisimple; 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; (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 thesis by A1; end; for x,y being Element of X st x\y=0.X holds x = y\(y\x) by A1; hence thesis by A2; end; theorem 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; 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; A2: (0.X\(x\y)) = (x\y)` .= 0.X by BCIALG_1:def 8; (x\(x\y)) = y\(y\x) by Def1; hence thesis by A2,BCIALG_1:2; end; for x,y being Element of X st x\y=0.X holds x = y\(y\x) by BCIALG_1:def 11,Th5; hence thesis by A1,Def4,Def5; end; theorem X is BCI-weakly-commutative BCI-algebra implies X is BCI-commutative proof assume A1: X is BCI-weakly-commutative BCI-algebra; let x,y be Element of X; assume x\y=0.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 thesis by BCIALG_1:2; end; theorem Th16: 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; 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))); let x,y be Element of X; assume x\y=0.X; then x\(x\y) = x by BCIALG_1:2; hence thesis by A2; 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; let x,y be Element of X; (x\(x\y))\y = (x\y)\(x\y) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; hence thesis by A3; end; hence thesis by A1; end; theorem Th17: 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; 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); 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; 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; 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 thesis by A3,BCIALG_1:def 7; end; hence thesis; 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; let x,y be Element of X; (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 thesis by BCIALG_1:def 5; end; hence thesis by A1; end; theorem for X being BCI-algebra holds (X is BCI-commutative iff for a being Element of AtomSet(X),x,y being Element of BranchV(a) holds x\(x\y) = y\(y\x) ) proof let X be BCI-algebra; thus X is BCI-commutative implies for a being Element of AtomSet(X), x,y being Element of BranchV(a) holds x\(x\y) = y\(y\x) proof assume A1: X is BCI-commutative; let a be Element of AtomSet(X); let x,y be Element of BranchV(a); 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; 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; then (x\(x\y))\(y\(y\x)) = 0.X by A1,Th17; hence thesis by A2,BCIALG_1:def 7; end; assume A3: for a being Element of AtomSet(X), x,y being Element of BranchV(a) holds x\(x\y) = y\(y\x); for x,y being Element of X holds (x\y=0.X implies x = y\(y\x)) proof let x,y be Element of X; set aa = 0.X\(0.X\x); aa``= aa by BCIALG_1:8; then A4: aa in AtomSet(X) by BCIALG_1:29; A5: aa\x = (0.X\x)\(0.X\x) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; then A6: aa<=x; assume A7: x\y=0.X; then aa\y = 0.X by A5,BCIALG_1:3; then aa<=y; then consider aa be 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 thesis by A7,BCIALG_1:2; end; hence thesis; end; theorem 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; (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))); for x,y being Element of X holds (x\y=0.X & y\x=0.X implies x = y) proof let x,y be Element of X; assume that A2: x\y=0.X and A3: y\x=0.X; A4: x\(x\y) = x by A1,A2; y\(y\(x\(x\y))) = y\0.X by A1,A2,A3 .= y by A1; hence thesis by A1,A4; end; then X is being_BCI-4; hence thesis by A1,Th16,BCIALG_1:11; end; hence thesis by Th16,BCIALG_1:1,2; end; theorem 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; 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; for x,z being Element of X holds (x\z=0.X implies x = z\(z\x)) proof let x,z be Element of X; set y = z\(z\x); (z\y)\(z\x) = (z\x)\(z\x) by BCIALG_1:8 .= 0.X by BCIALG_1:def 5; then A3: (z\y)<=(z\x); assume x\z=0.X; then x<=z; then x <= z\(z\x) by A2,A3; then A4: x\(z\(z\x)) = 0.X; (z\(z\x))\x = (z\x)\(z\x) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; hence thesis by A4,BCIALG_1:def 7; end; hence thesis; 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; 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; assume that A6: x<=z and A7: z\y<=z\x; x\z = 0.X by A6; then A8: x = z\(z\x) by A5; (z\y)\(z\x) = 0.X by A7; then 0.X = x\y by A8,BCIALG_1:7; hence thesis; end; hence thesis; end; hence thesis by A1; end; theorem 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; thus X is BCI-commutative implies for x,y,z being Element of X st x<=y & x<= z holds x<=y\(y\z) proof assume A1: X is BCI-commutative; 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; assume that A2: x<=y and A3: x<=z; A4: x\z = 0.X by A3; x\y = 0.X by A2; then A5: x = y\(y\x) by A1; 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 thesis; end; hence thesis; end; assume A6: for x,y,z being Element of X st x<=y & x<=z holds x<=y\(y\z); 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; x\x =0.X by BCIALG_1:def 5; then A7: x<=x; assume x\y=0.X; then x<=y; then x<=y\(y\x) by A6,A7; then A8: x\(y\(y\x)) = 0.X; (y\(y\x))\x = (y\x)\(y\x) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; hence thesis by A8,BCIALG_1:def 7; end; hence thesis; end; begin :: Several Classes of BCK-algebra---bounded BCK-algebra definition let IT be BCK-algebra; attr IT is bounded means ex a be Element of IT st a is being_greatest; end; registration cluster BCI-EXAMPLE -> bounded; coherence proof set IT = BCI-EXAMPLE; set a = the Element of IT; IT is bounded proof take a; for x being Element of IT holds x\a=0.IT by STRUCT_0:def 10; hence thesis; end; hence thesis; end; end; registration cluster bounded commutative for BCK-algebra; existence proof take BCI-EXAMPLE; thus thesis; end; end; definition let IT be bounded BCK-algebra; attr IT is involutory means for a being Element of IT st a is being_greatest holds for x being Element of IT holds a\(a\x)=x; end; theorem Th22: 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; 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) proof assume A1: X is involutory; let a be Element of X; assume A2: a is being_greatest; for x,y being Element of X holds x\y = (a\y)\(a\x) proof let x,y be Element of X; x\y = (a\(a\x))\y by A1,A2 .= (a\y)\(a\x) by BCIALG_1:7; hence thesis; end; hence thesis; 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); let a be Element of X; assume A4: a is being_greatest; now let x be Element of 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; end; hence thesis; end; theorem Th23: 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; 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) proof assume A1: X is involutory; let a be Element of X; assume A2: a is being_greatest; let x,y be Element of X; x\(a\y) = (a\(a\y))\(a\x) & y\(a\x) = (a\(a\x))\(a\y) by A1,A2,Th22; hence thesis by BCIALG_1:7; 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); let a be Element of X; assume A4: a is being_greatest; let x be Element of X; a\(a\x) = x\(a\a) by A3,A4 .= x\0.X by BCIALG_1:def 5 .= x by BCIALG_1:2; hence thesis; end; theorem 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 implies y <= a\x ) proof let X be bounded BCK-algebra; 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 by Th23; assume A1: 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; assume A2: a is being_greatest; let x be Element of X; (a\x)\(a\x) = 0.X by BCIALG_1:def 5; then (a\x)<=(a\x); then x <= a\(a\x) by A1,A2; then A3: x\(a\(a\x)) = 0.X; (a\(a\x))\x = (a\x)\(a\x) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; hence thesis by A3,BCIALG_1:def 7; end; definition let IT be BCK-algebra; let a be Element of IT; attr a is being_Iseki means for x being Element of IT holds x\a=0.IT & a\x=a; end; definition let IT be BCK-algebra; attr IT is Iseki_extension means ex a be Element of IT st a is being_Iseki; end; registration cluster BCI-EXAMPLE -> Iseki_extension; coherence proof set IT = BCI-EXAMPLE; IT is Iseki_extension proof set a = the Element of IT; take a; for x being Element of IT holds x\a=0.IT & a\x=a by STRUCT_0:def 10; hence thesis; end; hence thesis; end; end; :: Commutative Ideal definition let X be BCK-algebra; mode Commutative-Ideal of X -> non empty Subset of X means :Def10: 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 proof set X1 = BCK-part(X); A1: for x,y,z being Element of X st (x\y)\z in X1 & z in X1 holds x\(y\(y\ x)) in X1 proof let x,y,z be Element of X; assume that (x\y)\z in X1 and z in X1; 0.X\(x\(y\(y\x)))=(x\(y\(y\x)))` .= 0.X by BCIALG_1:def 8; then 0.X <= (x\(y\(y\x))); hence thesis; end; 0.X in X1 by BCIALG_1:19; hence thesis by A1; end; end; theorem 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 proof assume A1: IT is Commutative-Ideal of X; let x,y be Element of X; assume x\y in IT; then A2: (x\y)\0.X in IT by BCIALG_1:2; thus thesis by A1,A2,Def10; end; theorem Th26: for X being BCK-algebra st IT is Commutative-Ideal of X holds IT is Ideal of X proof let X be BCK-algebra; assume A1: IT is Commutative-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; assume that A3: x\y in IT and A4: y 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 thesis by A1,A4,A5,Def10; end; 0.X in IT by A1,Def10; hence thesis by A1,A2,BCIALG_1:def 18; end; theorem 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 proof assume IT is Commutative-Ideal of X; then A1: IT is Ideal of X by Th26; let x,y be Element of X; ((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); assume x\(x\y) in IT; hence thesis by A1,A2,BCIALG_1:46; end; begin :: Several Classes of BCK-algebra---implicative BCK-algebra definition let IT be BCK-algebra; attr IT is BCK-positive-implicative means :Def11: for x,y,z being Element of IT holds (x\y)\z=(x\z)\(y\z); attr IT is BCK-implicative means :Def12: for x,y being Element of IT holds x \(y\x)=x; end; registration cluster BCI-EXAMPLE -> BCK-positive-implicative BCK-implicative; coherence by STRUCT_0:def 10; end; registration cluster Iseki_extension BCK-positive-implicative BCK-implicative bounded commutative for BCK-algebra; existence proof take BCI-EXAMPLE; thus thesis; end; end; theorem Th28: X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y = (x\y)\y proof thus X is BCK-positive-implicative BCK-algebra implies for x,y being Element of X holds x\y = (x\y)\y proof assume A1: X is BCK-positive-implicative BCK-algebra; let x,y be Element of X; (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 thesis; end; assume A2: for x,y being Element of X holds x\y = (x\y)\y; 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; (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; then (x\z)\y <= (x\z)\(y\z) by BCIALG_1:5; then ((x\z)\y)\((x\z)\(y\z)) = 0.X; 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 thesis by A3,BCIALG_1:def 7; end; hence thesis by Def11; end; theorem Th29: 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 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))) proof assume A1: 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; (x\(x\y))\y = (x\y)\(x\y) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; then (x\(x\y)) <= y; 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; 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; 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; (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)); 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; (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; 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; then (x\(x\(y\(y\x))))\(x\(x\y)\(y\x)) = 0.X by A5,BCIALG_1:3; hence thesis by A3,BCIALG_1:def 7; end; hence thesis; end; assume A6: 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\y = (x\y)\y proof let x,y be Element of X; 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 thesis by A6,A7; end; hence thesis by Th28; end; theorem X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y = (x\y)\(x\(x\y)) proof thus X is BCK-positive-implicative BCK-algebra implies for x,y being Element of X holds x\y = (x\y)\(x\(x\y)) proof assume A1: X is BCK-positive-implicative BCK-algebra; let x,y be Element of X; 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 thesis by A1,A2,Th29; end; assume A3: for x,y being Element of X holds x\y = (x\y)\(x\(x\y)); for x,y being Element of X holds x\y = (x\y)\y proof let x,y be Element of X; (x\y)\(x\(x\y)) = (x\(x\(x\y)))\y by BCIALG_1:7 .= (x\y)\y by BCIALG_1:8; hence thesis by A3; end; hence thesis by Th28; end; theorem 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 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 proof assume A1: X is BCK-positive-implicative BCK-algebra; let x,y,z be Element of X; ((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 thesis; end; assume A2: for x,y,z being Element of X holds (x\z)\(y\z) <= (x\y)\z; 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; (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; 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; 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; hence thesis by A3,BCIALG_1:def 7; end; hence thesis by Def11; end; theorem X is BCK-positive-implicative BCK-algebra iff for x,y being Element of X holds x\y <= (x\y)\y proof thus X is BCK-positive-implicative BCK-algebra implies for x,y being Element of X holds x\y <= (x\y)\y proof assume A1: X is BCK-positive-implicative BCK-algebra; let x,y be Element of X; (x\y)\((x\y)\y) = ((x\y)\y)\((x\y)\y) by A1,Th28 .= 0.X by BCIALG_1:def 5; hence thesis; end; assume A2: for x,y being Element of X holds x\y <= (x\y)\y; for x,y being Element of X holds x\y = (x\y)\y proof let x,y be Element of X; x\y <= (x\y)\y by A2; then A3: (x\y)\((x\y)\y) = 0.X; ((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 thesis by A3,BCIALG_1:def 7; end; hence thesis by Th28; end; theorem 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 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) proof assume A1: X is BCK-positive-implicative BCK-algebra; let x,y be Element of 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 thesis; end; assume A2: 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; (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; ((x\(x\y))\(y\x))\(x\(x\(y\(y\x))))=0.X by BCIALG_1:10; hence thesis by A3,BCIALG_1:def 7; end; hence thesis by Th29; end; theorem Th34: X is BCK-implicative BCK-algebra iff X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra proof thus X is BCK-implicative BCK-algebra implies X is commutative BCK-algebra & X is BCK-positive-implicative BCK-algebra proof assume A1: X is BCK-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; (x\(x\y))\y = (x\y)\(x\y) by BCIALG_1:7 .= 0.X by BCIALG_1:def 5; then (x\(x\y)) <= y; 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 thesis by A1,Def12; end; for x,y being Element of X holds x\y = (x\y)\y proof let x,y be Element of X; (x\y)\(y\(x\y))=(x\y) by A1,Def12; hence thesis by A1,Def12; end; hence thesis by A2,Th1,Th28; end; assume that A3: X is commutative BCK-algebra and A4: X is BCK-positive-implicative BCK-algebra; for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of 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 thesis by A5,BCIALG_1:2; end; hence thesis by Def12; end; theorem Th35: X is BCK-implicative BCK-algebra iff for x,y being Element of X holds (x\(x\y))\(x\y) = (y\(y\x)) proof thus X is BCK-implicative BCK-algebra implies for x,y being Element of X holds (x\(x\y))\(x\y) = (y\(y\x)) proof assume A1: X is BCK-implicative BCK-algebra; let x,y be Element of 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 thesis by A1,Def12; end; assume A2: for x,y being Element of X holds (x\(x\y))\(x\y)=y\(y\x); for x,y being Element of X holds (x\y)\y = x\y proof let x,y be Element of X; 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 thesis by A3,A4,BCIALG_1:2; end; then A5: X is BCK-positive-implicative BCK-algebra by Th28; for x,y being Element of X holds ( x<= y implies x= y\(y\x) ) proof let x,y be Element of X; assume x<=y; then A6: x\y = 0.X; then (y\(y\x)) = (x\(x\y))\0.X by A2 .= (x\0.X) by A6,BCIALG_1:2; hence thesis by BCIALG_1:2; end; then X is commutative BCK-algebra by Th5; hence thesis by A5,Th34; end; theorem 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; 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) proof assume A1: X is BCK-implicative BCK-algebra; then A2: X is commutative BCK-algebra by Th34; let x,y,z be Element of X; 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 thesis by A3; 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); A5: for x,y being Element of X holds x\0.X = x proof let x,y be Element of X; 0.X\(0.X\0.X) = 0.X by A4; hence thesis by A4; 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; assume x\y=0.X & y\x=0.X; 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; 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; x\(x\y) = (x\0.X)\(x\y) by A5 .= ((y\0.X)\(y\x))\(x\y) by A4; hence thesis by A5; end; A8: for y being Element of X holds y\y = 0.X proof let y be Element of 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 thesis by A4; end; A9: for x being Element of X holds 0.X\x = 0.X proof let x be Element of X; (0.X\x)\(0.X\x) = 0.X\x by A4; hence thesis by A8; end; A10: for x,y being Element of X holds (x\y)\x = 0.X proof let x,y be Element of 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 thesis by A9; 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; (((y\z)\(y\x))\(x\y))\((y\z)\(y\x)) = 0.X by A10; hence thesis by A4; 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; ((y\z)\(y\x))\((x\z)\(x\y)) = 0.X & ((x\z)\(x\y))\((y\z)\(y\x)) = 0.X by A11; hence thesis by A6; 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; x\(x\y) = (y\(y\x)) by A13,Def1; hence thesis by A7; end; hence thesis by A4,A12,Th6,Th35; end; Lm1: for X being bounded BCK-algebra holds (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 ) proof let X be bounded BCK-algebra; assume X is BCK-implicative; then A1: X is commutative BCK-algebra by Th34; let a be Element of X; assume A2: a is being_greatest; let x be Element of X; a\(a\x) = x\(x\a) by A1,Def1 .= x\0.X by A2; hence thesis by BCIALG_1:2; end; theorem Th37: for X being bounded BCK-algebra,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; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies X is involutory & X is BCK-positive-implicative by Lm1,Th34; assume that A2: X is involutory and A3: X is BCK-positive-implicative; for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of X; y\a = 0.X by A1; then y<=a; then A4: y\x <= a\x by BCIALG_1:5; x\(a\x) = (a\(a\x))\(a\x) by A1,A2 .= a\(a\x) by A3,Th28 .= x by A1,A2; then x <= x\(y\x) by A4,BCIALG_1:5; then A5: x\(x\(y\x)) = 0.X; (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 thesis by A5,BCIALG_1:def 7; end; hence thesis; end; theorem X is BCK-implicative BCK-algebra iff for x,y being Element of X holds x\(x\(y\x)) = 0.X proof thus X is BCK-implicative BCK-algebra implies for x,y being Element of X holds x\(x\(y\x)) = 0.X proof assume A1: X is BCK-implicative BCK-algebra; let x,y be Element of X; x\(x\(y\x)) = x\x by A1,Def12; hence thesis by BCIALG_1:def 5; end; assume A2: for x,y being Element of X holds x\(x\(y\x)) = 0.X; for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of 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 thesis by A3,BCIALG_1:def 7; end; hence thesis by Def12; end; theorem 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 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))) proof assume A1: X is BCK-implicative BCK-algebra; let x,y be Element of X; 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 thesis by A1,Th35; end; assume A2: for x,y being Element of X holds (x\(x\y))\(x\y) = y\(y\(x\(x\y))); A3: for x,y being Element of X holds (x\y)\y = x\y proof let x,y be Element of X; 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 thesis by A2,A4; 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; x\(x\y) = (x\(x\y))\(x\y) by A3; hence thesis by A2; 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; (x\(x\y))\(x\y) = y\(y\(x\(x\y))) by A2 .= y\(y\(y\(y\x))) by A5,Def1; hence thesis by BCIALG_1:8; end; hence thesis by Th35; end; theorem Th40: 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 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) proof assume A1: X is BCK-implicative BCK-algebra; then A2: X is commutative BCK-algebra by Th34; let x,y,z be Element of X; 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 thesis by A3,Def11; end; assume A4: for x,y,z being Element of X holds (x\z)\(x\y)=(y\z)\((y\x)\z); A5: for x,y being Element of X holds x\(x\y)= y\(y\x) proof let x,y be Element of 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 thesis by BCIALG_1:2; 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; (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 thesis by A5; end; then for x,y being Element of X holds (x\(x\y))\(x\y) = y\(y\x); hence thesis by Th35; end; theorem 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 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)) proof assume A1: X is BCK-implicative BCK-algebra; 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; (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 thesis by A2,Def11; end; hence thesis; end; assume A3: for x,y,z being Element of X holds x\(x\(y\z)) = (y\z)\((y\z)\(x\z)); for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of 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 thesis by A4,BCIALG_1:def 7; end; hence thesis by Def12; end; theorem X is BCK-implicative BCK-algebra iff for x,y being Element of X holds (x\(x\y)) = (y\(y\x))\(x\y) proof thus X is BCK-implicative BCK-algebra implies for x,y being Element of X holds (x\(x\y)) = (y\(y\x))\(x\y) proof assume A1: X is BCK-implicative BCK-algebra; 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; (x\(x\y))\(x\y) = y\(y\x) by A1,Th35; then (y\(y\x))\(x\y) = y\(y\x) by A2,Def1; hence thesis by A2,Def1; end; hence thesis; end; assume A3: for x,y being Element of X holds (x\(x\y)) = (y\(y\x))\(x\y); for x,y being Element of X st x<= y holds x= y\(y\x) proof let x,y be Element of X; assume x<=y; then x\y = 0.X; then (x\0.X) = (y\(y\x))\0.X by A3; then (x\0.X) = y\(y\x) by BCIALG_1:2; hence thesis by BCIALG_1:2; 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; 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 thesis by BCIALG_1:8; end; then X is BCK-positive-implicative BCK-algebra by Th28; hence thesis by A4,Th34; end; theorem Th43: for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x being Element of X holds (a\x)\((a\x )\x) = 0.X proof assume A2: X is BCK-implicative; let x be Element of X; (a\x)\((a\x)\x) = x\(x\(a\x)) by Def1 .= x\x by A2; hence thesis by BCIALG_1:def 5; end; assume A3: for x being Element of X holds (a\x)\((a\x)\x) = 0.X; for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of 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; then y<=a; 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; (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 thesis by A6,BCIALG_1:def 7; end; hence thesis; end; theorem for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x being Element of X holds x\(a\x) = x; assume A2: for x being Element of X holds x\(a\x) = x; for x,y being Element of X holds x\(y\x)=x proof let x,y be Element of X; A3: (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; then y<=a; then y\x <= a\x by BCIALG_1:5; then A4: x\(a\x) <= x\(y\x) by BCIALG_1:5; x\(x\(a\x)) = x\x by A2 .= 0.X by BCIALG_1:def 5; then x\(a\x) = x by A3,BCIALG_1:def 7; then A5: x\(x\(y\x)) = 0.X by A4; (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 thesis by A5,BCIALG_1:def 7; end; hence thesis; end; theorem for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x being Element of X holds (a\x)\x = ( a\x) proof assume A2: X is BCK-implicative; let x be Element of 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 thesis by A3,BCIALG_1:def 7; end; assume A4: for x being Element of X holds (a\x)\x = (a\x); let x,y be Element of 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; then y<=a; 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; (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 thesis by A7,BCIALG_1:def 7; end; theorem Th46: for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x,y being Element of X holds (a\y)\((a \y)\x) = x\y proof assume A2: X is BCK-implicative; let x,y be Element of X; X is involutory by 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; then x\y <= (a\y)\((a\y)\x) by A4,BCIALG_1:5; then A5: (x\y)\((a\y)\((a\y)\x)) = 0.X; 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 thesis by A5,BCIALG_1:def 7; end; assume A6: for x,y being Element of X holds (a\y)\((a\y)\x) = x\y; for x being Element of X holds (a\x)\((a\x)\x) = 0.X proof let x be Element of X; (a\x)\((a\x)\x) = x\x by A6; hence thesis by BCIALG_1:def 5; end; hence thesis by A1,Th43; end; theorem Th47: for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x,y being Element of X holds y\(y\x) = x\(a\y) proof assume A2: X is BCK-implicative; let x,y be Element of X; 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 thesis by BCIALG_1:8; end; assume A3: for x,y being Element of X holds y\(y\x) = x\(a\y); for x,y being Element of X holds (a\y)\((a\y)\x) = x\y proof let x,y be Element of X; (a\y)\((a\y)\x) = x\(a\(a\y)) by A3 .= x\(y\(y\a)) by Def1 .= x\(y\0.X) by A1; hence thesis by BCIALG_1:2; end; hence thesis by A1,Th46; end; theorem for X being bounded commutative BCK-algebra,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 bounded commutative BCK-algebra; let a be Element of X; assume A1: a is being_greatest; thus X is BCK-implicative implies for x,y,z being Element of X holds (x\(y\z ))\(x\y) <= x\(a\z) proof assume A2: X is BCK-implicative; let x,y,z be Element of X; 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 thesis; end; assume A5: for x,y,z being Element of X holds (x\(y\z))\(x\y) <= x\(a\z); for x being Element of X holds (a\x)\((a\x)\x) = 0.X proof let x be Element of 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; hence thesis by Def1; end; hence thesis by A1,Th43; end;