let X be BCI-algebra; :: thesis: for A, I being Ideal of X
for IA being I-congruence of X,A
for II being I-congruence of X,I st Class IA,(0. X) = Class II,(0. X) holds
IA = II
let A, I be Ideal of X; :: thesis: for IA being I-congruence of X,A
for II being I-congruence of X,I st Class IA,(0. X) = Class II,(0. X) holds
IA = II
let IA be I-congruence of X,A; :: thesis: for II being I-congruence of X,I st Class IA,(0. X) = Class II,(0. X) holds
IA = II
let II be I-congruence of X,I; :: thesis: ( Class IA,(0. X) = Class II,(0. X) implies IA = II )
assume A1:
Class IA,(0. X) = Class II,(0. X)
; :: thesis: IA = II
let xx, yy be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [xx,yy] in IA or [xx,yy] in II ) & ( not [xx,yy] in II or [xx,yy] in IA ) )
thus
( [xx,yy] in IA implies [xx,yy] in II )
:: thesis: ( not [xx,yy] in II or [xx,yy] in IA )proof
assume A2:
[xx,yy] in IA
;
:: thesis: [xx,yy] in II
then consider x,
y being
set such that A3:
(
[xx,yy] = [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 A3;
A4:
(
y \ x in II .: {(0. X)} &
x \ y in II .: {(0. X)} )
by A1, A2, A3, Th40;
then consider z being
set such that A5:
(
[z,(y \ x)] in II &
z in {(0. X)} )
by RELAT_1:def 13;
[(0. X),(y \ x)] in II
by A5, TARSKI:def 1;
then
(y \ x) \ (0. X) in I
by Def12;
then A6:
y \ x in I
by BCIALG_1:2;
consider z being
set such that A7:
(
[z,(x \ y)] in II &
z in {(0. X)} )
by A4, RELAT_1:def 13;
[(0. X),(x \ y)] in II
by A7, TARSKI:def 1;
then
(x \ y) \ (0. X) in I
by Def12;
then
x \ y in I
by BCIALG_1:2;
hence
[xx,yy] in II
by A3, A6, Def12;
:: thesis: verum
end;
thus
( [xx,yy] in II implies [xx,yy] in IA )
:: thesis: verumproof
assume A8:
[xx,yy] in II
;
:: thesis: [xx,yy] in IA
then consider x,
y being
set such that A9:
(
[xx,yy] = [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 A9;
A10:
(
y \ x in IA .: {(0. X)} &
x \ y in IA .: {(0. X)} )
by A1, A8, A9, Th40;
then consider z being
set such that A11:
(
[z,(y \ x)] in IA &
z in {(0. X)} )
by RELAT_1:def 13;
[(0. X),(y \ x)] in IA
by A11, TARSKI:def 1;
then
(y \ x) \ (0. X) in A
by Def12;
then A12:
y \ x in A
by BCIALG_1:2;
consider z being
set such that A13:
(
[z,(x \ y)] in IA &
z in {(0. X)} )
by A10, RELAT_1:def 13;
[(0. X),(x \ y)] in IA
by A13, TARSKI:def 1;
then
(x \ y) \ (0. X) in A
by Def12;
then
x \ y in A
by BCIALG_1:2;
hence
[xx,yy] in IA
by A9, A12, Def12;
:: thesis: verum
end;