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

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

end;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

hence
I is commutative Ideal of X
by A1, Th34; :: thesis: verum
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;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