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 BCI-algebra
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 BCI-algebra
let K be closed Ideal of X; :: thesis: for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra
let RK be I-congruence of X,K; :: thesis: HK (G,RK) is BCI-algebra
reconsider IT = HK (G,RK) as non empty BCIStr_0 ;
A1: IT is being_BCI-4

proof

let x, y be Element of IT; :: according to BCIALG_1:def 7 :: thesis: ( not x \ y = 0. IT or not y \ x = 0. IT or x = y )
reconsider x1 = x, y1 = y as Element of Union (G,RK) ;
reconsider x2 = x1, y2 = y1 as Element of X ;
assume ( x \ y = 0. IT & y \ x = 0. IT ) ; :: thesis: x = y
then ( x2 \ y2 = 0. X & y2 \ x2 = 0. X ) by Def12;
hence x = y by BCIALG_1:def 7; :: thesis: verum

end;

A2: now :: thesis: for x, y, z being Element of IT holds ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT

let x, y, z be Element of IT; :: thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT
reconsider x1 = x, y1 = y, z1 = z as Element of Union (G,RK) ;
reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X ;
( x2 \ y2 = x1 \ y1 & z2 \ y2 = z1 \ y1 ) by Def12;
then A3: (x2 \ y2) \ (z2 \ y2) = (x1 \ y1) \ (z1 \ y1) by Def12;
x2 \ z2 = x1 \ z1 by Def12;
then ((x2 \ y2) \ (z2 \ y2)) \ (x2 \ z2) = ((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1) by A3, Def12;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT by BCIALG_1:def 3; :: thesis: verum

end;

A4: IT is being_C

proof

let x, y, z be Element of IT; :: according to BCIALG_1:def 4 :: thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT
reconsider x1 = x, y1 = y, z1 = z as Element of Union (G,RK) ;
reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X ;
x2 \ z2 = x1 \ z1 by Def12;
then A5: (x2 \ z2) \ y2 = (x1 \ z1) \ y1 by Def12;
x2 \ y2 = x1 \ y1 by Def12;
then (x2 \ y2) \ z2 = (x1 \ y1) \ z1 by Def12;
then ((x2 \ y2) \ z2) \ ((x2 \ z2) \ y2) = ((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1) by A5, Def12;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT by BCIALG_1:def 4; :: thesis: verum

end;

IT is being_I

proof

let x be Element of IT; :: according to BCIALG_1:def 5 :: thesis: x \ x = 0. IT
reconsider x1 = x as Element of Union (G,RK) ;
reconsider x2 = x1 as Element of X ;
x2 \ x2 = x1 \ x1 by Def12;
hence x \ x = 0. IT by BCIALG_1:def 5; :: thesis: verum

end;

hence HK (G,RK) is BCI-algebra by A2, A4, A1, BCIALG_1:def 3; :: thesis: verum