let X be BCI-algebra; for I being Ideal of X
for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let I be Ideal of X; for RI being I-congruence of X,I
for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let RI be I-congruence of X,I; for E being Congruence of X st ( for LC being L-congruence of X holds LC is I-congruence of X,I ) holds
E = RI
let E be Congruence of X; ( ( for LC being L-congruence of X holds LC is I-congruence of X,I ) implies E = RI )
assume A1:
for LC being L-congruence of X holds LC is I-congruence of X,I
; E = RI
let x1, y1 be object ; RELAT_1:def 2 ( ( not [x1,y1] in E or [x1,y1] in RI ) & ( not [x1,y1] in RI or [x1,y1] in E ) )
E is L-congruence of X
by Th36;
then A2:
E is I-congruence of X,I
by A1;
thus
( [x1,y1] in E implies [x1,y1] in RI )
( not [x1,y1] in RI or [x1,y1] in E )proof
assume A3:
[x1,y1] in E
;
[x1,y1] in RI
then consider x,
y being
object such that A4:
[x1,y1] = [x,y]
and A5:
(
x in the
carrier of
X &
y in the
carrier of
X )
by RELSET_1:2;
reconsider x =
x,
y =
y as
Element of
X by A5;
y \ x in Class (
E,
(0. X))
by A3, A4, Th40;
then
ex
z being
object st
(
[z,(y \ x)] in E &
z in {(0. X)} )
by RELAT_1:def 13;
then
[(0. X),(y \ x)] in E
by TARSKI:def 1;
then
(y \ x) \ (0. X) in I
by A2, Def12;
then A6:
y \ x in I
by BCIALG_1:2;
x \ y in Class (
E,
(0. X))
by A3, A4, Th40;
then
ex
z being
object st
(
[z,(x \ y)] in E &
z in {(0. X)} )
by RELAT_1:def 13;
then
[(0. X),(x \ y)] in E
by TARSKI:def 1;
then
(x \ y) \ (0. X) in I
by A2, Def12;
then
x \ y in I
by BCIALG_1:2;
hence
[x1,y1] in RI
by A4, A6, Def12;
verum
end;
thus
( [x1,y1] in RI implies [x1,y1] in E )
verumproof
assume A7:
[x1,y1] in RI
;
[x1,y1] in E
then consider x,
y being
object such that A8:
[x1,y1] = [x,y]
and A9:
(
x in the
carrier of
X &
y in the
carrier of
X )
by RELSET_1:2;
reconsider x =
x,
y =
y as
Element of
X by A9;
(
x \ y in I &
y \ x in I )
by A7, A8, Def12;
hence
[x1,y1] in E
by A2, A8, Def12;
verum
end;