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 )

then {(0. X)} is commutative Ideal of X by Th35;

hence X is commutative BCK-algebra by Th36; :: thesis: verum

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
for I being Ideal of X holds I is commutative Ideal of X
; :: thesis: X is commutative BCK-algebra
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;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

then {(0. X)} is commutative Ideal of X by Th35;

hence X is commutative BCK-algebra by Th36; :: thesis: verum