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: 0. G = 0. X by BCIALG_1:def 10;
then c1: 0. G in K by BCIALG_1:def 18;
then C1: 0. G in the carrier of G /\ K by XBOOLE_0:def 4;
for x being set st x in the carrier of G /\ K holds
x in the carrier of G by XBOOLE_0:def 4;
then C2: the carrier of G /\ K is non empty Subset of G by c1, TARSKI:def 3, XBOOLE_0:def 4;
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 ( x \ y in the carrier of G /\ K & y in the carrier of G /\ K ) ; :: thesis: x in the carrier of G /\ K
then D3: ( x \ y in K & y in K ) by XBOOLE_0:def 4;
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider x1 = x, y1 = y as Element of X by TARSKI:def 3;
( x1 \ y1 in K & y1 in K ) by Lmth14, D3;
then x in K by BCIALG_1:def 18;
hence x in the carrier of G /\ K by XBOOLE_0:def 4; :: thesis: verum

end;

then reconsider GK = the carrier of G /\ K as Ideal of G by C1, C2, 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
D1: ( x in the carrier of G & x in K ) by XBOOLE_0:def 4;
then reconsider y = x as Element of X ;
y ` in K by D1, BCIALG_1:def 19;
then x ` in K by Lmth14, A1;
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