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:90;
then A1: dom (the InternalDiff of X || the carrier of (HK G,RK)) = [:D,D:] by XBOOLE_1:28, ZFMISC_1:119;
for y being set holds
( y in D iff 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

let y be set ; :: thesis: ( y in D iff 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 ) )

A2: now

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 set 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:70;
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:106;
then (the InternalDiff of X || the carrier of (HK G,RK)) . [y,(0. (HK G,RK))] = y1 \ y2 by FUNCT_1:72
.= 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 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 A2; :: thesis: verum

end;

then rng (the InternalDiff of X || the carrier of (HK G,RK)) = D by FUNCT_1:def 5;
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:11;
set B = the InternalDiff of (HK G,RK);

now

let x, y be Element of the carrier of (HK G,RK); :: thesis: A . x,y = the InternalDiff of (HK G,RK) . x,y
reconsider xx = x, yy = y as Element of Union G,RK ;
( 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:72;
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) ) by BINOP_1:2;
hence HK G,RK is SubAlgebra of X by BCIALG_1:def 10; :: thesis: verum