let X be BCI-algebra; :: thesis: for G being SubAlgebra of X
for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G
let G be SubAlgebra of X; :: thesis: for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G
let K be closed Ideal of X; :: thesis: the carrier of G /\ K is closed Ideal of G
set GK = the carrier of G /\ K;
A1: for x, y being Element of G st x \ y in the carrier of G /\ K & y in the carrier of G /\ K holds
x in the carrier of G /\ K

proof

let x, y be Element of G; :: thesis: ( x \ y in the carrier of G /\ K & y in the carrier of G /\ K implies x in the carrier of G /\ K )
assume that
A2: x \ y in the carrier of G /\ K and
A3: y in the carrier of G /\ K ; :: thesis: x in the carrier of G /\ K
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider x1 = x, y1 = y as Element of X ;
x \ y in K by A2, XBOOLE_0:def 4;
then A4: x1 \ y1 in K by Th34;
y1 in K by A3, XBOOLE_0:def 4;
then x in K by A4, BCIALG_1:def 18;
hence x in the carrier of G /\ K by XBOOLE_0:def 4; :: thesis: verum

end;

A5: 0. G = 0. X by BCIALG_1:def 10;
then A6: 0. G in K by BCIALG_1:def 18;
then A7: 0. G in the carrier of G /\ K by XBOOLE_0:def 4;
for x being object st x in the carrier of G /\ K holds
x in the carrier of G by XBOOLE_0:def 4;
then the carrier of G /\ K is non empty Subset of G by A6, TARSKI:def 3, XBOOLE_0:def 4;
then reconsider GK = the carrier of G /\ K as Ideal of G by A7, A1, BCIALG_1:def 18;
for x being Element of GK holds x ` in GK

proof

let x be Element of GK; :: thesis: x ` in GK
A8: x in K by XBOOLE_0:def 4;
then reconsider y = x as Element of X ;
y ` in K by A8, BCIALG_1:def 19;
then x ` in K by A5, Th34;
hence x ` in GK by XBOOLE_0:def 4; :: thesis: verum

end;

hence the carrier of G /\ K is closed Ideal of G by BCIALG_1:def 19; :: thesis: verum