let X be BCI-algebra; :: thesis: for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X
let G be SubAlgebra of X; :: thesis: for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X
let K be closed Ideal of X; :: thesis: for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X
let RK be I-congruence of X,K; :: thesis: HK (G,RK) is SubAlgebra of X
set IT = HK (G,RK);
set V1 = the carrier of (HK (G,RK));
reconsider D = the carrier of (HK (G,RK)) as non empty set ;
set A = the InternalDiff of X || the carrier of (HK (G,RK));
set VV = the carrier of X;
dom the InternalDiff of X = [: the carrier of X, the carrier of X:] by FUNCT_2:def 1;
then dom ( the InternalDiff of X || the carrier of (HK (G,RK))) = [: the carrier of X, the carrier of X:] /\ [: the carrier of (HK (G,RK)), the carrier of (HK (G,RK)):] by RELAT_1:61;
then A1: dom ( the InternalDiff of X || the carrier of (HK (G,RK))) = [:D,D:] by XBOOLE_1:28, ZFMISC_1:96;
for y being object holds
( y in D iff ex z being object st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) )

proof

let y be object ; :: thesis: ( y in D iff ex z being object st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) )

A2: now :: thesis: ( ex z being set st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) implies y in D )

given z being set such that A3: z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) and
A4: y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ; :: thesis: y in D
consider x1, x2 being object such that
A5: ( x1 in D & x2 in D ) and
A6: z = [x1,x2] by A1, A3, ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of Union (G,RK) by A5;
reconsider v1 = x1, v2 = x2 as Element of the carrier of X ;
y = v1 \ v2 by A3, A4, A6, FUNCT_1:47;
then y = x1 \ x2 by Def12;
hence y in D ; :: thesis: verum

end;

( y in D implies ex z being set st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) )

proof

assume A7: y in D ; :: thesis: ex z being set st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z )
then reconsider y1 = y, y2 = 0. (HK (G,RK)) as Element of X ;
A8: [y,(0. (HK (G,RK)))] in [:D,D:] by A7, ZFMISC_1:87;
then ( the InternalDiff of X || the carrier of (HK (G,RK))) . [y,(0. (HK (G,RK)))] = y1 \ y2 by FUNCT_1:49
.= y by BCIALG_1:2 ;
hence ex z being set st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) by A1, A8; :: thesis: verum

end;

hence ( y in D iff ex z being object st
( z in dom ( the InternalDiff of X || the carrier of (HK (G,RK))) & y = ( the InternalDiff of X || the carrier of (HK (G,RK))) . z ) ) by A2; :: thesis: verum

end;

then rng ( the InternalDiff of X || the carrier of (HK (G,RK))) = D by FUNCT_1:def 3;
then reconsider A = the InternalDiff of X || the carrier of (HK (G,RK)) as BinOp of the carrier of (HK (G,RK)) by A1, FUNCT_2:def 1, RELSET_1:4;
set B = the InternalDiff of (HK (G,RK));

now :: thesis: for x, y being Element of the carrier of (HK (G,RK)) holds A . (x,y) = the InternalDiff of (HK (G,RK)) . (x,y)

let x, y be Element of the carrier of (HK (G,RK)); :: thesis: A . (x,y) = the InternalDiff of (HK (G,RK)) . (x,y)
( x in the carrier of (HK (G,RK)) & y in the carrier of (HK (G,RK)) ) ;
then reconsider vx = x, vy = y as Element of the carrier of X ;
[x,y] in [: the carrier of (HK (G,RK)), the carrier of (HK (G,RK)):] by ZFMISC_1:def 2;
then A . (x,y) = vx \ vy by FUNCT_1:49;
hence A . (x,y) = the InternalDiff of (HK (G,RK)) . (x,y) by Def12; :: thesis: verum

end;

then ( 0. (HK (G,RK)) = 0. X & A = the InternalDiff of (HK (G,RK)) ) ;
hence HK (G,RK) is SubAlgebra of X by BCIALG_1:def 10; :: thesis: verum