let X be BCI-algebra; :: thesis: {(0. X)} is Ideal of X

set X1 = {(0. X)};

A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds

x in {(0. X)}

hence {(0. X)} is Ideal of X by A1, A2, Def18; :: thesis: verum

set X1 = {(0. X)};

now :: thesis: for xx being object st xx in {(0. X)} holds

xx in the carrier of X

then A1:
{(0. X)} is Subset of X
by TARSKI:def 3;xx in the carrier of X

let xx be object ; :: thesis: ( xx in {(0. X)} implies xx in the carrier of X )

assume xx in {(0. X)} ; :: thesis: xx in the carrier of X

then xx = 0. X by TARSKI:def 1;

hence xx in the carrier of X ; :: thesis: verum

end;assume xx in {(0. X)} ; :: thesis: xx in the carrier of X

then xx = 0. X by TARSKI:def 1;

hence xx in the carrier of X ; :: thesis: verum

A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds

x in {(0. X)}

proof

0. X in {(0. X)}
by TARSKI:def 1;
set X1 = {(0. X)};

let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )

assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}

then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;

then x = 0. X by Th2;

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

end;let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )

assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}

then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;

then x = 0. X by Th2;

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

hence {(0. X)} is Ideal of X by A1, A2, Def18; :: thesis: verum