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