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 object ; :: 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 object such that
A3: [xx,yy] = [x,y] and
A4: ( 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 A4;
x \ y in II .: {(0. X)} by A1, A2, A3, Th40;
then ex z being object st
( [z,(x \ y)] in II & z in {(0. X)} ) by RELAT_1:def 13;
then [(0. X),(x \ y)] in II by TARSKI:def 1;
then (x \ y) \ (0. X) in I by Def12;
then A5: x \ y in I by BCIALG_1:2;
y \ x in II .: {(0. X)} by A1, A2, A3, Th40;
then ex z being object st
( [z,(y \ x)] in II & z in {(0. X)} ) by RELAT_1:def 13;
then [(0. X),(y \ x)] in II by TARSKI:def 1;
then (y \ x) \ (0. X) in I by Def12;
then y \ x in I by BCIALG_1:2;
hence [xx,yy] in II by A3, A5, Def12; :: thesis: verum
end;
thus ( [xx,yy] in II implies [xx,yy] in IA ) :: thesis: verum
proof
assume A6: [xx,yy] in II ; :: thesis: [xx,yy] in IA
then consider x, y being object such that
A7: [xx,yy] = [x,y] and
A8: ( 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 A8;
x \ y in IA .: {(0. X)} by A1, A6, A7, Th40;
then ex z being object st
( [z,(x \ y)] in IA & z in {(0. X)} ) by RELAT_1:def 13;
then [(0. X),(x \ y)] in IA by TARSKI:def 1;
then (x \ y) \ (0. X) in A by Def12;
then A9: x \ y in A by BCIALG_1:2;
y \ x in IA .: {(0. X)} by A1, A6, A7, Th40;
then ex z being object st
( [z,(y \ x)] in IA & z in {(0. X)} ) by RELAT_1:def 13;
then [(0. X),(y \ x)] in IA by TARSKI:def 1;
then (y \ x) \ (0. X) in A by Def12;
then y \ x in A by BCIALG_1:2;
hence [xx,yy] in IA by A7, A9, Def12; :: thesis: verum
end;