let X be BCI-algebra; :: thesis: for X1 being Ideal of X st X1 = {(0. X)} holds

for x being Element of X1 holds x ` in {(0. X)}

let X1 be Ideal of X; :: thesis: ( X1 = {(0. X)} implies for x being Element of X1 holds x ` in {(0. X)} )

assume A1: X1 = {(0. X)} ; :: thesis: for x being Element of X1 holds x ` in {(0. X)}

let x be Element of X1; :: thesis: x ` in {(0. X)}

x = 0. X by A1, TARSKI:def 1;

then x ` = 0. X by Def5;

hence x ` in {(0. X)} by TARSKI:def 1; :: thesis: verum

for x being Element of X1 holds x ` in {(0. X)}

let X1 be Ideal of X; :: thesis: ( X1 = {(0. X)} implies for x being Element of X1 holds x ` in {(0. X)} )

assume A1: X1 = {(0. X)} ; :: thesis: for x being Element of X1 holds x ` in {(0. X)}

let x be Element of X1; :: thesis: x ` in {(0. X)}

x = 0. X by A1, TARSKI:def 1;

then x ` = 0. X by Def5;

hence x ` in {(0. X)} by TARSKI:def 1; :: thesis: verum