let X be BCI-algebra; :: thesis: BCK-part X is closed Ideal of X
set X1 = BCK-part X;
A1: 0. X in BCK-part X by Th19;
for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X

proof

let x, y be Element of X; :: thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume A2: ( x \ y in BCK-part X & y in BCK-part X ) ; :: thesis: x in BCK-part X
consider x1 being Element of X such that
A3: ( x \ y = x1 & 0. X <= x1 ) by A2;
consider x2 being Element of X such that
A4: ( y = x2 & 0. X <= x2 ) by A2;
(x \ y) ` = 0. X by A3, Def11;
then (x ` ) \ (y ` ) = 0. X by Th9;
then (x ` ) \ (0. X) = 0. X by A4, Def11;
then x ` = 0. X by Th2;
then 0. X <= x by Def11;
hence x in BCK-part X ; :: thesis: verum

end;

then reconsider X1 = BCK-part X as Ideal of X by A1, Def18;

now

let x be Element of X1; :: thesis: x ` in X1
x in X1 ;
then consider x1 being Element of X such that
A5: ( x = x1 & 0. X <= x1 ) ;
x ` = 0. X by A5, Def11;
then (x ` ) ` = 0. X by Def5;
then 0. X <= x ` by Def11;
hence x ` in X1 ; :: thesis: verum

end;

hence BCK-part X is closed Ideal of X by Def19; :: thesis: verum