let X be BCK-algebra; :: thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) iff {(0. X)} is commutative Ideal of X )
thus ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies {(0. X)} is commutative Ideal of X ) by BCIALG_1:43; :: thesis: ( {(0. X)} is commutative Ideal of X implies 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: verum
proof
assume A1: {(0. X)} is commutative Ideal of X ; :: thesis: for I being Ideal of X holds I is commutative Ideal of X
let I be Ideal of X; :: thesis: I is commutative Ideal of X
for I being Ideal of X holds {(0. X)} c= I
proof
let I be Ideal of X; :: thesis: {(0. X)} c= I
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. X)} or x in I )
assume x in {(0. X)} ; :: thesis: x in I
then x = 0. X by TARSKI:def 1;
hence x in I by BCIALG_1:def 18; :: thesis: verum
end;
hence I is commutative Ideal of X by A1, Th34; :: thesis: verum
end;