let X be BCK-algebra; :: thesis: ( {(0. X)} is commutative Ideal of X iff for I being Ideal of X holds I is commutative Ideal of X )
thus ( {(0. X)} is commutative Ideal of X implies for I being Ideal of X holds I is commutative Ideal of X ) :: thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X )

proof

assume {(0. X)} is commutative Ideal of X ; :: thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by Th36;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; :: thesis: verum

end;

assume for I being Ideal of X holds I is commutative Ideal of X ; :: thesis: {(0. X)} is commutative Ideal of X
then X is commutative BCK-algebra by Th37;
hence {(0. X)} is commutative Ideal of X by Th36; :: thesis: verum