let X be BCI-algebra; for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let I be Ideal of X; for RI being I-congruence of X,I holds X ./. RI is BCI-algebra
let RI be I-congruence of X,I; X ./. RI is BCI-algebra
reconsider IT = X ./. RI as non empty BCIStr_0 ;
A1:
now for w1, w2, w3 being Element of IT holds ((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. ITlet w1,
w2,
w3 be
Element of
IT;
((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. IT
w1 in the
carrier of
IT
;
then consider x1 being
object such that A2:
x1 in the
carrier of
X
and A3:
w1 = Class (
RI,
x1)
by EQREL_1:def 3;
w3 in the
carrier of
IT
;
then consider z1 being
object such that A4:
z1 in the
carrier of
X
and A5:
w3 = Class (
RI,
z1)
by EQREL_1:def 3;
w2 in the
carrier of
IT
;
then consider y1 being
object such that A6:
y1 in the
carrier of
X
and A7:
w2 = Class (
RI,
y1)
by EQREL_1:def 3;
reconsider x1 =
x1,
y1 =
y1,
z1 =
z1 as
Element of
X by A2, A6, A4;
A8:
w3 \ w2 = Class (
RI,
(z1 \ y1))
by A7, A5, Def17;
w1 \ w2 = Class (
RI,
(x1 \ y1))
by A3, A7, Def17;
then A9:
(w1 \ w2) \ (w3 \ w2) = Class (
RI,
((x1 \ y1) \ (z1 \ y1)))
by A8, Def17;
w1 \ w3 = Class (
RI,
(x1 \ z1))
by A3, A5, Def17;
then
((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = Class (
RI,
(((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1)))
by A9, Def17;
hence
((w1 \ w2) \ (w3 \ w2)) \ (w1 \ w3) = 0. IT
by BCIALG_1:def 3;
verum end;
A10:
now for w1, w2, w3 being Element of IT holds ((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. ITlet w1,
w2,
w3 be
Element of
IT;
((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. IT
w1 in the
carrier of
IT
;
then consider x1 being
object such that A11:
x1 in the
carrier of
X
and A12:
w1 = Class (
RI,
x1)
by EQREL_1:def 3;
w2 in the
carrier of
IT
;
then consider y1 being
object such that A13:
y1 in the
carrier of
X
and A14:
w2 = Class (
RI,
y1)
by EQREL_1:def 3;
w3 in the
carrier of
IT
;
then consider z1 being
object such that A15:
z1 in the
carrier of
X
and A16:
w3 = Class (
RI,
z1)
by EQREL_1:def 3;
reconsider x1 =
x1,
y1 =
y1,
z1 =
z1 as
Element of
X by A11, A13, A15;
w1 \ w3 = Class (
RI,
(x1 \ z1))
by A12, A16, Def17;
then A17:
(w1 \ w3) \ w2 = Class (
RI,
((x1 \ z1) \ y1))
by A14, Def17;
w1 \ w2 = Class (
RI,
(x1 \ y1))
by A12, A14, Def17;
then
(w1 \ w2) \ w3 = Class (
RI,
((x1 \ y1) \ z1))
by A16, Def17;
then
((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = Class (
RI,
(((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1)))
by A17, Def17;
hence
((w1 \ w2) \ w3) \ ((w1 \ w3) \ w2) = 0. IT
by BCIALG_1:def 4;
verum end;
A18:
now for w1, w2 being Element of IT st w1 \ w2 = 0. IT & w2 \ w1 = 0. IT holds
w1 = w2let w1,
w2 be
Element of
IT;
( w1 \ w2 = 0. IT & w2 \ w1 = 0. IT implies w1 = w2 )assume that A19:
w1 \ w2 = 0. IT
and A20:
w2 \ w1 = 0. IT
;
w1 = w2
w1 in the
carrier of
IT
;
then consider x1 being
object such that A21:
x1 in the
carrier of
X
and A22:
w1 = Class (
RI,
x1)
by EQREL_1:def 3;
w2 in the
carrier of
IT
;
then consider y1 being
object such that A23:
y1 in the
carrier of
X
and A24:
w2 = Class (
RI,
y1)
by EQREL_1:def 3;
reconsider x1 =
x1,
y1 =
y1 as
Element of
X by A21, A23;
w2 \ w1 = Class (
RI,
(y1 \ x1))
by A22, A24, Def17;
then
0. X in Class (
RI,
(y1 \ x1))
by A20, EQREL_1:23;
then
[(y1 \ x1),(0. X)] in RI
by EQREL_1:18;
then
(y1 \ x1) \ (0. X) in I
by Def12;
then A25:
y1 \ x1 in I
by BCIALG_1:2;
w1 \ w2 = Class (
RI,
(x1 \ y1))
by A22, A24, Def17;
then
0. X in Class (
RI,
(x1 \ y1))
by A19, EQREL_1:23;
then
[(x1 \ y1),(0. X)] in RI
by EQREL_1:18;
then
(x1 \ y1) \ (0. X) in I
by Def12;
then
x1 \ y1 in I
by BCIALG_1:2;
then
[x1,y1] in RI
by A25, Def12;
hence
w1 = w2
by A22, A24, EQREL_1:35;
verum end;
hence
X ./. RI is BCI-algebra
by A1, A10, A18, BCIALG_1:def 3, BCIALG_1:def 4, BCIALG_1:def 5, BCIALG_1:def 7; verum