let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
thus ( X is commutative BCK-algebra 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 X is commutative BCK-algebra )
proof
assume X is commutative BCK-algebra ; :: thesis: for I being Ideal of X holds I is commutative Ideal of X
then {(0. X)} is commutative Ideal of X by Th36;
hence for I being Ideal of X holds I is commutative Ideal of X by Th35; :: thesis: verum
end;
assume for I being Ideal of X holds I is commutative Ideal of X ; :: thesis: X is commutative BCK-algebra
then {(0. X)} is commutative Ideal of X by Th35;
hence X is commutative BCK-algebra by Th36; :: thesis: verum