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