let X be BCI-algebra; :: thesis: for P being non empty Subset of X
for X being BCI-algebra st P = p-Semisimple-part X holds
( X is BCK-algebra iff P = {(0. X)} )
let P be non empty Subset of X; :: thesis: for X being BCI-algebra st P = p-Semisimple-part X holds
( X is BCK-algebra iff P = {(0. X)} )
let X be BCI-algebra; :: thesis: ( P = p-Semisimple-part X implies ( X is BCK-algebra iff P = {(0. X)} ) )
assume A1: P = p-Semisimple-part X ; :: thesis: ( X is BCK-algebra iff P = {(0. X)} )
thus ( X is BCK-algebra implies P = {(0. X)} ) :: thesis: ( P = {(0. X)} implies X is BCK-algebra )

proof

assume A2: X is BCK-algebra ; :: thesis: P = {(0. X)}
thus P c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in {(0. X)} )
assume B1: x in P ; :: thesis: x in {(0. X)}
consider x1 being Element of X such that
B2: ( x = x1 & x1 is minimal ) by A1, B1;
reconsider x = x as Element of X by B2;
(0. X) \ x = x `
.= 0. X by A2, BCIALG_1:def 8 ;
then x = 0. X by B2, BCIALG_1:def 14;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

D1: 0. X in P by A1;
for x being set st x in {(0. X)} holds
x in P by D1, TARSKI:def 1;
hence {(0. X)} c= P by TARSKI:def 3; :: thesis: verum

end;

assume A2: P = {(0. X)} ; :: thesis: X is BCK-algebra
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 in P by A2, TARSKI:def 1;
then (0. X) \ x in P by A1, BCIALG_1:33;
hence (0. X) \ x = 0. X by A2, TARSKI:def 1; :: thesis: verum

end;

then for x being Element of X holds x ` = 0. X ;
hence X is BCK-algebra by BCIALG_1:def 8; :: thesis: verum