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 ;
C1: IT is being_B

proof

now

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 ;
AA: ( x2 \ y2 = x1 \ y1 & z2 \ y2 = z1 \ y1 & x2 \ z2 = x1 \ z1 ) by Def6;
then (x2 \ y2) \ (z2 \ y2) = (x1 \ y1) \ (z1 \ y1) by Def6;
then ((x2 \ y2) \ (z2 \ y2)) \ (x2 \ z2) = ((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1) by AA, Def6;
hence ((x \ y) \ (z \ y)) \ (x \ z) = 0. IT by BCIALG_1:def 3; :: thesis: verum

end;

hence IT is being_B by BCIALG_1:def 3; :: thesis: verum

end;

C3: 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 \ y2 = x1 \ y1 & x2 \ z2 = x1 \ z1 ) by Def6;
then ( (x2 \ y2) \ z2 = (x1 \ y1) \ z1 & (x2 \ z2) \ y2 = (x1 \ z1) \ y1 ) by Def6;
then ((x2 \ y2) \ z2) \ ((x2 \ z2) \ y2) = ((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1) by Def6;
hence ((x \ y) \ z) \ ((x \ z) \ y) = 0. IT by BCIALG_1:def 4; :: thesis: verum

end;

C5: 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 Def6;
hence x \ x = 0. IT by BCIALG_1:def 5; :: thesis: verum

end;

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 )
assume D1: ( x \ y = 0. IT & y \ x = 0. IT ) ; :: thesis: x = y
reconsider x1 = x, y1 = y as Element of Union G,RK ;
reconsider x2 = x1, y2 = y1 as Element of X ;
( x2 \ y2 = 0. X & y2 \ x2 = 0. X ) by D1, Def6;
hence x = y by BCIALG_1:def 7; :: thesis: verum

end;

hence HK G,RK is BCI-algebra by C1, C3, C5; :: thesis: verum