:: Congruences and Quotient Algebras of {BCI}-algebras
:: by Yuzhong Ding and Zhiyong Pang
::
:: Received August 28, 2007
:: Copyright (c) 2007-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies BCIALG_1, CARD_FIL, SUBSET_1, FUNCT_1, NUMBERS, STRUCT_0, POWER,
CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, FUNCOP_1, NAT_1, SUPINF_2, RELAT_1,
CHORD, WAYBEL15, GROUP_4, GROUP_1, ALG_1, EQREL_1, PARTFUN1, RELAT_2,
ZFMISC_1, RCOMP_1, TARSKI, BINOP_1, GROUP_6, BCIALG_2, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, XCMPLX_0, NAT_1, FUNCT_2, XXREAL_0, FUNCOP_1, BINOP_1, STRUCT_0,
BCIALG_1, RELAT_2, PARTFUN1, EQREL_1, ALG_1;
constructors BCIALG_1, BINOP_1, NAT_1, BINARITH, EQREL_1, RELSET_1, XREAL_0,
NUMBERS, FUNCOP_1;
registrations BCIALG_1, SUBSET_1, NAT_1, RELSET_1, STRUCT_0, PARTFUN1,
ORDINAL1, XREAL_0, CARD_1;
requirements NUMERALS, ARITHM, SUBSET, BOOLE;
definitions XBOOLE_0, TARSKI, RELAT_1;
equalities STRUCT_0, BCIALG_1, RELAT_1;
expansions BCIALG_1;
theorems BCIALG_1, FUNCOP_1, NAT_1, XREAL_1, TARSKI, XBOOLE_0, RELAT_2,
RELAT_1, XXREAL_0, ORDERS_1, XBOOLE_1, BINOP_1, EQREL_1, RELSET_1,
ZFMISC_1, ORDINAL1;
schemes FUNCT_2, NAT_1, RELSET_1, XBOOLE_0, BINOP_1;
begin :: Basic Properties of The Element P16-P19
reserve X for BCI-algebra;
reserve I for Ideal of X;
reserve a,x,y,z,u for Element of X;
reserve f,f9,g for sequence of the carrier of X;
reserve j,i,k,n,m for Nat;
:: x*y to_power n = x*y|^n
:: n=0: it=x; n=1:it =x*y; n=2:it=(x*y)*y...
definition
let X,x,y;
let n be Nat;
func (x,y) to_power n -> Element of X means
:Def1:
ex f st it = f.n & f.0 = x & for j being Nat st jx as sequence of the carrier of X;
take u = f.n;
take f9 = f;
thus u = f9.n & f9.0 = x by FUNCOP_1:7;
thus for j being Nat st j positive minimal;
coherence by Lm2,Lm3;
end;
theorem
a is minimal iff for x holds a\x=x`\a`
proof
thus a is minimal implies for x holds a\x=x`\a`
proof
assume
A1: a is minimal;
let x;
x\(x\a)\a=0.X by BCIALG_1:1;
then x\(x\a)<=a;
then
A2: (a\x)\(x`\a`)=((x\(x\a))\x)\(x`\a`)by A1
.=((x\x)\(x\a))\(x`\a`) by BCIALG_1:7
.=((x\a)`)\(x`\a`) by BCIALG_1:def 5
.=((x\a)`)\((x\a)`) by BCIALG_1:9
.=0.X by BCIALG_1:def 5;
(x`\a`)\(a\x)=0.X by BCIALG_1:1;
hence thesis by A2,BCIALG_1:def 7;
end;
thus (for x holds a\x=x`\a`) implies a is minimal
proof
assume
A3: for x holds a\x=x`\a`;
now
let x;
assume x<=a;
then
A4: x\a=0.X;
a\x=x`\a` by A3;
then a\x=(0.X)` by A4,BCIALG_1:9;
then a\x=0.X by BCIALG_1:def 5;
hence a=x by A4,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
x` is minimal iff for y holds y<=x implies x` = y`
proof
thus x` is minimal implies for y holds y<=x implies x` = y`
proof
assume
A1: x` is minimal;
let y;
assume y<=x;
then y\x=0.X;
then (y\x)`=0.X by BCIALG_1:def 5;
then y`\x`=0.X by BCIALG_1:9;
then y`<=x`;
hence thesis by A1;
end;
thus (for y holds y<=x implies x` = y`)implies x` is minimal
proof
assume
A2: for y holds y<=x implies x` = y`;
now
let xx be Element of X;
assume xx<=x`;
then
A3: xx\x`=0.X;
then (xx\x`)`=0.X by BCIALG_1:def 5;
then xx`\((x`)`)=0.X by BCIALG_1:9;
then (xx`\((x`)`))`=0.X by BCIALG_1:def 5;
then ((xx`)`)\(((x`)`)`)=0.X by BCIALG_1:9;
then ((xx`)`)\x`=0.X by BCIALG_1:8;
then (xx`\x)`=0.X by BCIALG_1:9;
then (x`\xx)`=0.X by BCIALG_1:7;
then (xx\xx)\(x`\xx)=0.X by BCIALG_1:def 5;
then (xx\x`)`=0.X by BCIALG_1:def 3;
then xx`\((x`)`)=0.X by BCIALG_1:9;
then xx`\x\(((x`)`)\x)=0.X by BCIALG_1:4;
then xx`\x\0.X=0.X by BCIALG_1:1;
then xx`\x=0.X by BCIALG_1:2;
then xx`<=x;
then (xx`)`=x` by A2;
then 0.X = x`\xx by BCIALG_1:1;
hence xx=x` by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
x` is minimal iff for y,z holds (((x\z)\(y\z))`)` = y`\x`
proof
thus x` is minimal implies for y,z holds (((x\z)\(y\z))`)` = y`\x`
proof
assume
A1: x` is minimal;
let y,z;
y`\(x\y)\x`=0.X by BCIALG_1:def 3;
then
A2: y`\(x\y)<=x`;
(((x\z)\(y\z))`)` = ((x\z)`\(y\z)`)` by BCIALG_1:9
.= ((x`\z`)\((y\z)`))` by BCIALG_1:9;
then (((x\z)\(y\z))`)` = ((y`\(x\y)\z`)\(y\z)`)` by A1,A2
.= ((y`\z`\(x\y))\(y\z)`)` by BCIALG_1:7
.= (((y\z)`\(x\y))\(y\z)`)` by BCIALG_1:9
.= (((y\z)`)\((y\z)`)\(x\y))` by BCIALG_1:7
.= ((x\y)`)` by BCIALG_1:def 5
.= (x`\y`)` by BCIALG_1:9
.= ((y`)`\x)` by BCIALG_1:7
.= ((y`)`)`\x` by BCIALG_1:9
.= y`\x` by BCIALG_1:8;
hence thesis;
end;
thus (for y,z holds (((x\z)\(y\z))`)` = y`\x`) implies x` is minimal
proof
assume
A3: for y,z holds (((x\z)\(y\z))`)` = y`\x`;
now
let x1 be Element of X;
assume x1<=x`;
then
A4: x1\x`=0.X;
then (x1`\x`)\(x1`\x1)=0.X by BCIALG_1:4;
then ((((x\0.X)\(x1\0.X))`)`)\(x1`\x1)=0.X by A3;
then ((x1`\x1)`)\(((x\0.X)\(x1\0.X))`)=0.X by BCIALG_1:7;
then ((x1`\x1)`)\((x\(x1\0.X))`)=0.X by BCIALG_1:2;
then ((x1`\x1)`)\((x\x1)`)=0.X by BCIALG_1:2;
then (((x1`)`)\x1`)\((x\x1)`)=0.X by BCIALG_1:9;
then (((x1`)`)\x1`)\(x`\x1`)=0.X by BCIALG_1:9;
then (((x1`)`)\x`)`=0.X by BCIALG_1:def 3;
then (((x1`)`)`)\((x`)`)=0.X by BCIALG_1:9;
then x1`\((x`)`)=0.X by BCIALG_1:8;
then (((x`)`)`)\x1=0.X by BCIALG_1:7;
then x`\x1=0.X by BCIALG_1:8;
hence x1=x` by A4,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
end;
theorem
0.X is maximal implies for a holds a is minimal
proof
assume
A1: 0.X is maximal;
let a;
now
let x;
assume x<=a;
then
A2: x\a=0.X;
then (a\x)`=0.X by BCIALG_1:6;
then 0.X <= a\x;
then 0.X = a\x by A1;
hence x=a by A2,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
theorem
(ex x st x is greatest) implies for a holds a is positive
proof
given x such that
A1: x is greatest;
let a;
a<=x by A1;
then a\x=0.X;
then
A2: (a\x)`=0.X by BCIALG_1:def 5;
0.X<=x by A1;
then x`=0.X;
then a`\0.X=0.X by A2,BCIALG_1:9;
then a`=0.X by BCIALG_1:2;
then 0.X<=a;
hence thesis;
end;
theorem Th28:
x\(x``) is positive Element of X
proof
(x\((x`)`))` = x`\(((x`)`)`) by BCIALG_1:9
.=x`\x` by BCIALG_1:8
.=0.X by BCIALG_1:def 5;
then 0.X<=x\((x`)`);
hence thesis by Def2;
end;
theorem
a is minimal iff a`` = a
proof
thus a is minimal implies a`` = a
proof
(a`)`\a=0.X by BCIALG_1:1;
then
A1: (a`)` <= a;
assume a is minimal;
hence thesis by A1;
end;
assume
A2: a`` = a;
now
let x;
assume x<=a;
then
A3: x\a=0.X;
a\x=x`\a` by A2,BCIALG_1:7;
then a\x=(0.X)` by A3,BCIALG_1:9;
then a\x=0.X by BCIALG_1:def 5;
hence x=a by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
theorem Th30:
a is minimal iff ex x st a=x`
proof
thus a is minimal implies ex x st a=x`
proof
assume
A1: a is minimal;
take x=a`;
x`\a=0.X by BCIALG_1:1;
then x` <= a;
hence thesis by A1;
end;
given x such that
A2: a=x`;
now
let y;
assume y<=a;
then
A3: y\a=0.X;
then a\y=y\x`\y\x by A2,BCIALG_1:7;
then a\y=y\y\x`\x by BCIALG_1:7;
then a\y=(x`)`\x by BCIALG_1:def 5;
then a\y=0.X by BCIALG_1:1;
hence a=y by A3,BCIALG_1:def 7;
end;
hence thesis by Lm1;
end;
:: p38
definition
let X,x;
attr x is nilpotent means
ex k being non zero Nat st (0.X ,x) to_power k = 0.X;
end;
definition
let X;
attr X is nilpotent means
for x being Element of X holds x is nilpotent;
end;
definition
let X,x;
assume
A1: x is nilpotent;
func ord x -> non zero Nat means
:Def8:
(0.X,x) to_power it = 0.
X & for m being Nat st (0.X,x) to_power m=0.X & m <> 0 holds it <= m;
existence
proof
defpred P[Nat] means ex w be Nat st w=$1 & (0.X,x)to_power w =
0.X & w<>0;
ex k being non zero Nat st (0.X,x) to_power k = 0.X by A1;
then
A2: ex n being Nat st P[n];
consider k being Nat such that
A3: P[k] and
A4: for n being Nat st P[n] holds k <= n from NAT_1:sch 5(A2);
reconsider k as non zero Nat by A3;
take k;
thus thesis by A3,A4;
end;
uniqueness
proof
let n1,n2 be non zero Nat;
assume (0.X,x) to_power n1 = 0.X & ( for m being Nat st (0.X,x
) to_power m=0.X&m <> 0 holds n1 <=m)& ( 0.X,x) to_power n2 = 0.X & for m being
Nat st (0.X,x)to_power m=0.X&m <> 0 holds n2 <=m;
then n1 <= n2 & n2 <= n1;
hence thesis by XXREAL_0:1;
end;
correctness;
end;
registration
let X;
cluster 0.X -> nilpotent;
coherence
proof
(0.X,0.X) to_power 1 = 0.X by Th6;
hence thesis;
end;
end;
theorem :: P39
x is positive Element of X iff x is nilpotent & ord x=1
proof
thus x is positive Element of X implies x is nilpotent&ord x=1
proof
assume x is positive Element of X;
then 0.X<=x by Def2;
then
A1: x`=0.X;
thus
A2: x is nilpotent
proof
set k=1;
take k;
thus thesis by A1,Th2;
end;
thus ord x=1
proof
set k=1;
reconsider k as non zero Nat;
(0.X,x) to_power k=0.X & for m being Nat st (0.X,x)
to_power m=0.X &m <> 0 holds k<= m by A1,Th2,NAT_1:14;
hence thesis by A2,Def8;
end;
end;
assume x is nilpotent & ord x=1;
then (0.X,x) to_power 1 = 0.X by Def8;
then x`=0.X by Th2;
then 0.X<=x;
hence thesis by Def2;
end;
theorem
X is BCK-algebra iff for x holds ord x=1 & x is nilpotent
proof
thus X is BCK-algebra implies for x being Element of X holds ord x=1&x is
nilpotent
proof
set k=1;
assume
A1: X is BCK-algebra;
let x be Element of X;
A2: x`=0.X by A1,BCIALG_1:def 8;
then (0.X,x)to_power 1=0.X by Th2;
then
A3: x is nilpotent;
reconsider k as non zero Nat;
A4: for m being Nat st (0.X,x)to_power m=0.X&m <> 0 holds k<= m
by NAT_1:14;
(0.X,x) to_power k=0.X by A2,Th2;
hence thesis by A3,A4,Def8;
end;
assume
A5: for x holds ord x = 1&x is nilpotent;
now
let x;
ord x =1 & x is nilpotent by A5;
then (0.X,x) to_power 1 = 0.X by Def8;
hence x` =0.X by Th2;
end;
hence thesis by BCIALG_1:def 8;
end;
theorem
(0.X,x`) to_power n is minimal
proof
(0.X,x`) to_power n=((0.X,x) to_power n)` by Th9;
hence thesis by Th30;
end;
theorem
x is nilpotent implies ord x = ord (x`)
proof
assume
A1: x is nilpotent;
then consider k being non zero Nat such that
A2: (0.X,x) to_power k = 0.X;
A3: x` is nilpotent
proof
take k;
(0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
.=0.X by A2,BCIALG_1:def 5;
hence thesis;
end;
set k=ord x;
A4: now
let m be Nat;
assume that
A5: (0.X,x`)to_power m=0.X and
A6: m <> 0;
((0.X,x)to_power m)`=0.X by A5,Th9;
then (((0.X,x)to_power m)`)`=0.X by BCIALG_1:def 5;
then (0.X,x)to_power m=0.X by Th12;
hence k<=m by A1,A6,Def8;
end;
(0.X,x`) to_power k = ((0.X,x) to_power k)` by Th9
.=(0.X)` by A1,Def8
.=0.X by BCIALG_1:def 5;
hence thesis by A3,A4,Def8;
end;
begin :: Congruence and Quotient Algebras P58-65
definition
let X be BCI-algebra;
mode Congruence of X -> Equivalence_Relation of X means
:Def9:
for x,y,u,v
being Element of X st [x,y] in it & [u,v] in it holds [x\u,y\v] in it;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y,u,v be Element of X;
assume [x,y] in P & [u,v]in P;
then x=y & u=v by RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
:: Left Congruence
definition
let X be BCI-algebra;
mode L-congruence of X -> Equivalence_Relation of X means
:Def10:
for x,y
being Element of X st [x,y] in it holds for u being Element of X holds [u\x,u\y
] in it;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y be Element of X;
assume
A1: [x,y] in P;
let u be Element of X;
u\x=u\y by A1,RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
:: Right Congruence
definition
let X be BCI-algebra;
mode R-congruence of X -> Equivalence_Relation of X means
:Def11:
for x,y
being Element of X st [x,y] in it holds for u being Element of X holds [x\u,y\u
] in it;
existence
proof
reconsider P = id the carrier of X as Equivalence_Relation of X;
take P;
let x,y be Element of X;
assume
A1: [x,y] in P;
let u be Element of X;
x\u=y\u by A1,RELAT_1:def 10;
hence thesis by RELAT_1:def 10;
end;
end;
::Ideal Congruence
definition
let X be BCI-algebra,A be Ideal of X;
mode I-congruence of X,A -> Relation of X means
:Def12:
for x,y being Element of X holds [x,y] in it iff x\y in A & y\x in A;
existence
proof
defpred PP[object,object] means
ex x,y being Element of X st x=$1&y=$2 &x\y in A
& y\x in A;
consider P being Relation of X such that
A1: for x2,y2 being object holds [x2,y2] in P iff x2 in the carrier of X&
y2 in the carrier of X&PP[x2,y2] from RELSET_1:sch 1;
take P;
let x2,y2 be Element of X;
[x2,y2] in P implies ex x1,y1 being Element of X st x1=x2&y1=y2&x1\y1
in A & y1\x1 in A by A1;
hence [x2,y2] in P implies x2\y2 in A & y2\x2 in A;
thus thesis by A1;
end;
end;
registration
let X be BCI-algebra, A be Ideal of X;
cluster -> total symmetric transitive for I-congruence of X,A;
coherence
proof
for RI being I-congruence of X,A holds RI is Equivalence_Relation of X
proof
let RI be I-congruence of X,A;
reconsider RI as Relation of X;
for x being object st x in the carrier of X holds [x,x] in RI
proof
let x be object;
assume x in the carrier of X;
then reconsider x as Element of X;
0.X in A by BCIALG_1:def 18;
then x\x in A by BCIALG_1:def 5;
hence thesis by Def12;
end;
then RI is_reflexive_in the carrier of X by RELAT_2:def 1;
then
A1: field RI = the carrier of X by ORDERS_1:13;
for x,y,z being object st [x,y] in RI&[y,z] in RI holds [x,z] in RI
proof
let x,y,z be object;
assume that
A2: [x,y] in RI and
A3: [y,z] in RI;
reconsider x,y,z as Element of X by A2,A3,ZFMISC_1:87;
(z\x\(y\x))\(z\y)=0.X by BCIALG_1:def 3;
then
A4: (z\x\(y\x))\(z\y) in A by BCIALG_1:def 18;
(x\z\(x\y))\(y\z)=0.X by BCIALG_1:1;
then
A5: (x\z\(x\y))\(y\z) in A by BCIALG_1:def 18;
y\z in A by A3,Def12;
then
A6: x\z\(x\y) in A by A5,BCIALG_1:def 18;
z\y in A by A3,Def12;
then
A7: z\x\(y\x) in A by A4,BCIALG_1:def 18;
y\x in A by A2,Def12;
then
A8: z\x in A by A7,BCIALG_1:def 18;
x\y in A by A2,Def12;
then x\z in A by A6,BCIALG_1:def 18;
hence thesis by A8,Def12;
end;
then
A9: RI is transitive by RELAT_2:31;
for x,y being object st x in the carrier of X & y in the carrier of X &
[x,y] in RI holds [y,x] in RI
proof
let x,y be object;
assume that
A10: x in the carrier of X & y in the carrier of X and
A11: [x,y] in RI;
reconsider x,y as Element of X by A10;
x\y in A & y\x in A by A11,Def12;
hence thesis by Def12;
end;
then RI is_symmetric_in the carrier of X by RELAT_2:def 3;
then RI is symmetric by A1,RELAT_2:def 11;
hence thesis by A1,A9,EQREL_1:9;
end;
hence thesis;
end;
end;
definition
let X be BCI-algebra;
func IConSet(X) -> set means
:Def13:
for A1 being set holds A1 in it iff ex I being
Ideal of X st A1 is I-congruence of X,I;
existence
proof
defpred P[object] means
ex I being Ideal of X st $1 is I-congruence of X,I;
consider Y being set such that
A1: for x being object holds x in Y iff x in bool [:the carrier of X,the
carrier of X:] & P[x] from XBOOLE_0:sch 1;
take Y;
let x be set;
thus x in Y implies ex I being Ideal of X st x is I-congruence of X,I by A1
;
given I being Ideal of X such that
A2: x is I-congruence of X,I;
thus thesis by A1,A2;
end;
uniqueness
proof
defpred P[object] means
ex I being Ideal of X st $1 is I-congruence of X,I;
let A1, A2 be set such that
A3: for x being set holds x in A1 iff ex I being Ideal of X st x is
I-congruence of X,I and
A4: for x being set holds x in A2 iff ex I being Ideal of X st x is
I-congruence of X,I;
A5: for x being object holds x in A2 iff P[x] by A4;
A6: for x being object holds x in A1 iff P[x] by A3;
A1 = A2 from XBOOLE_0:sch 2(A6,A5);
hence thesis;
end;
end;
definition
let X be BCI-algebra;
func ConSet(X) -> set equals
the set of all R where R is Congruence of X;
coherence;
func LConSet(X) -> set equals
the set of all R where R is L-congruence of X;
coherence;
func RConSet(X) -> set equals
the set of all R where R is R-congruence of X;
coherence;
end;
reserve R for Equivalence_Relation of X;
reserve RI for I-congruence of X,I;
reserve E for Congruence of X;
reserve RC for R-congruence of X;
reserve LC for L-congruence of X;
:: huang-P58:P1.5.1
theorem
for X,E holds Class(E,0.X) is closed Ideal of X
proof
let X,E;
A1: now
let x,y be Element of X;
assume that
A2: x\y in Class(E,0.X) and
A3: y in Class(E,0.X);
A4: [x,x] in E by EQREL_1:5;
[0.X,y] in E by A3,EQREL_1:18;
then [x\0.X,x\y] in E by A4,Def9;
then [x,x\y] in E by BCIALG_1:2;
then
A5: [x\y,x] in E by EQREL_1:6;
[0.X,x\y] in E by A2,EQREL_1:18;
then [0.X,x] in E by A5,EQREL_1:7;
hence x in Class(E,0.X)by EQREL_1:18;
end;
A6: [0.X,0.X] in E by EQREL_1:5;
then 0.X in Class(E,0.X) by EQREL_1:18;
then reconsider Rx=Class(E,0.X) as Ideal of X by A1,BCIALG_1:def 18;
now
let x be Element of Rx;
[0.X,x] in E by EQREL_1:18;
then [(0.X)`,x`] in E by A6,Def9;
then [0.X,x`] in E by BCIALG_1:def 5;
hence x` in Class(E,0.X) by EQREL_1:18;
end;
hence thesis by BCIALG_1:def 19;
end;
theorem Th36:
R is Congruence of X iff R is R-congruence of X&R is L-congruence of X
proof
A1: field R = the carrier of X by EQREL_1:9;
then
A2: R is_reflexive_in the carrier of X by RELAT_2:def 9;
thus R is Congruence of X implies R is R-congruence of X&R is L-congruence
of X
proof
assume
A3: R is Congruence of X;
thus R is R-congruence of X
proof
let x,y be Element of X;
assume
A4: [x,y] in R;
let u be Element of X;
[u,u] in R by A2,RELAT_2:def 1;
hence thesis by A3,A4,Def9;
end;
let x,y be Element of X;
assume
A5: [x,y] in R;
let u be Element of X;
[u,u] in R by A2,RELAT_2:def 1;
hence thesis by A3,A5,Def9;
end;
assume
A6: R is R-congruence of X & R is L-congruence of X;
A7: R is_transitive_in the carrier of X by A1,RELAT_2:def 16;
now
let x,y,u,v be Element of X;
assume [x,y] in R & [u,v]in R;
then [x\u,y\u] in R & [y\u,y\v] in R by A6,Def10,Def11;
hence [x\u,y\v] in R by A7,RELAT_2:def 8;
end;
hence thesis by Def9;
end;
theorem Th37:
RI is Congruence of X
proof
field RI = the carrier of X by EQREL_1:9;
then
A1: RI is_transitive_in the carrier of X by RELAT_2:def 16;
now
let x,y,u,v be Element of X;
assume that
A2: [x,y] in RI and
A3: [u,v]in RI;
(y\u\(y\v))\(v\u)=0.X by BCIALG_1:1;
then
A4: (y\u\(y\v))\(v\u) in I by BCIALG_1:def 18;
v\u in I by A3,Def12;
then
A5: y\u\(y\v) in I by A4,BCIALG_1:def 18;
(y\v\(y\u))\(u\v)=0.X by BCIALG_1:1;
then
A6: (y\v\(y\u))\(u\v) in I by BCIALG_1:def 18;
u\v in I by A3,Def12;
then y\v\(y\u) in I by A6,BCIALG_1:def 18;
then
A7: [y\u,y\v] in RI by A5,Def12;
(x\u\(y\u))\(x\y)=0.X by BCIALG_1:def 3;
then
A8: (x\u\(y\u))\(x\y) in I by BCIALG_1:def 18;
(y\u\(x\u))\(y\x)=0.X by BCIALG_1:def 3;
then
A9: (y\u\(x\u))\(y\x) in I by BCIALG_1:def 18;
y\x in I by A2,Def12;
then
A10: y\u\(x\u) in I by A9,BCIALG_1:def 18;
x\y in I by A2,Def12;
then x\u\(y\u) in I by A8,BCIALG_1:def 18;
then [x\u,y\u] in RI by A10,Def12;
hence [x\u,y\v] in RI by A1,A7,RELAT_2:def 8;
end;
hence thesis by Def9;
end;
definition
let X be BCI-algebra, I be Ideal of X;
redefine mode I-congruence of X,I -> Congruence of X;
coherence by Th37;
end;
theorem Th38:
Class(RI,0.X) c= I
proof
let x be object;
assume
A1: x in Class(RI,0.X);
then consider y being object such that
A2: [y,x] in RI and
A3: y in {0.X} by RELAT_1:def 13;
reconsider x as Element of X by A1;
reconsider y as Element of X by A3,TARSKI:def 1;
y=0.X by A3,TARSKI:def 1;
then x\0.X in I by A2,Def12;
hence thesis by BCIALG_1:2;
end;
theorem
I is closed iff I = Class(RI,0.X)
proof
thus I is closed implies I = Class(RI,0.X)
proof
assume
A1: I is closed;
thus I c= Class(RI,0.X)
proof
let x be object;
assume
A2: x in I;
then reconsider x as Element of I;
A3: x\0.X in I by A2,BCIALG_1:2;
x` in I by A1;
then 0.X in {0.X} & [0.X,x] in RI by A3,Def12,TARSKI:def 1;
hence thesis by RELAT_1:def 13;
end;
thus thesis by Th38;
end;
assume
A4: I = Class(RI,0.X);
now
let x be Element of I;
ex y being object st [y,x] in RI & y in {0.X} by A4,RELAT_1:def 13;
then [0.X,x] in RI by TARSKI:def 1;
hence x` in I by Def12;
end;
hence thesis;
end;
theorem Th40:
[x,y] in E implies x\y in Class(E,0.X) & y\x in Class(E,0.X)
proof
assume
A1: [x,y] in E;
A2: field E = the carrier of X by EQREL_1:9;
then
A3: E is_reflexive_in the carrier of X by RELAT_2:def 9;
then
A4: [y,y] in E by RELAT_2:def 1;
E is_symmetric_in the carrier of X by A2,RELAT_2:def 11;
then [y,x] in E by A1,RELAT_2:def 3;
then [y\y,x\y] in E by A4,Def9;
then
A5: [0.X,x\y] in E by BCIALG_1:def 5;
[x,x] in E by A3,RELAT_2:def 1;
then [x\x,y\x] in E by A1,Def9;
then 0.X in {0.X} & [0.X,y\x] in E by BCIALG_1:def 5,TARSKI:def 1;
hence thesis by A5,RELAT_1:def 13;
end;
theorem
for A,I being Ideal of X,IA being I-congruence of X,A, II being
I-congruence of X,I st Class(IA,0.X)=Class(II,0.X) holds IA = II
proof
let A,I be Ideal of X,IA be I-congruence of X,A,II be I-congruence of X,I;
assume
A1: Class(IA,0.X) = Class(II,0.X);
let xx,yy be object;
thus [xx,yy] in IA implies [xx,yy] in II
proof
assume
A2: [xx,yy] in IA;
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,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 thesis by A3,A5,Def12;
end;
thus [xx,yy] in II implies [xx,yy] in IA
proof
assume
A6: [xx,yy] in II;
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,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 thesis by A7,A9,Def12;
end;
end;
theorem Th42:
[x,y] in E & u in Class(E,0.X) implies [x,(y,u)to_power k] in E
proof
assume that
A1: [x,y] in E and
A2: u in Class(E,0.X);
defpred P[Nat] means [x,(y,u)to_power $1] in E;
ex z being object st [z,u] in E & z in {0.X} by A2,RELAT_1:def 13;
then
A3: [0.X,u] in E by TARSKI:def 1;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [x,(y,u) to_power k] in E;
then [x\0.X,(y,u)to_power k\u] in E by A3,Def9;
then [x,(y,u)to_power k\u] in E by BCIALG_1:2;
hence thesis by Th4;
end;
A5: P[0] by A1,Th1;
for n holds P[n] from NAT_1:sch 2(A5,A4);
hence thesis;
end;
theorem
(for X,x,y holds ex i,j,m,n st ((x,x\y) to_power i,y\x) to_power j = (
(y,y\x)to_power m,x\y) to_power n) implies for E,I st I=Class(E,0.X) holds E is
I-congruence of X,I
proof
assume
A1: for X,x,y holds ex i,j,m,n st ((x,x\y)to_power i,y\x)to_power j =((y
,y\x)to_power m,x\y)to_power n;
let E,I;
assume
A2: I=Class(E,0.X);
now
let x,y be Element of X;
x\y in I & y\x in I implies[x,y] in E
proof
assume that
A3: x\y in I and
A4: y\x in I;
ex z being object st [z,y\x] in E & z in {0.X} by A2,A4,RELAT_1:def 13;
then
A5: [0.X,y\x] in E by TARSKI:def 1;
ex z being object st [z,x\y] in E & z in {0.X} by A2,A3,RELAT_1:def 13;
then
A6: [0.X,x\y] in E by TARSKI:def 1;
consider i,j,m,n being Nat such that
A7: ((x,x\y)to_power i,y\x)to_power j =((y,y\x)to_power m,x\y)
to_power n by A1;
A8: field E = the carrier of X by EQREL_1:9;
A9: E is_reflexive_in field E by RELAT_2:def 9;
then [x,x] in E by A8,RELAT_2:def 1;
then
A10: [x,(x,x\y) to_power i] in E by A2,A3,Th42;
A11: [x,((x,(x\y))to_power i,y\x)to_power j] in E
proof
defpred P[Nat] means [x,((x,(x\y))to_power i,y\x)to_power $1] in E;
A12: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [x,((x,(x\y))to_power i,y\x)to_power k] in E;
then [x\0.X,((x,(x\y))to_power i,y\x)to_power k\(y\x)] in E by A5
,Def9;
then [x,((x,(x\y))to_power i,y\x)to_power k\(y\x)] in E by BCIALG_1:2
;
hence thesis by Th4;
end;
A13: P[0] by A10,Th1;
for n holds P[n] from NAT_1:sch 2(A13,A12);
hence thesis;
end;
[y,y] in E by A8,A9,RELAT_2:def 1;
then
A14: [y,(y,y\x) to_power m] in E by A2,A4,Th42;
A15: [y,((y,(y\x))to_power m,x\y)to_power n] in E
proof
defpred P[Nat] means [y,((y,(y\x))to_power m,x\y)to_power $1] in E;
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume [y,((y,(y\x))to_power m,x\y)to_power k] in E;
then [y\0.X,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by A6
,Def9;
then [y,((y,(y\x))to_power m,x\y)to_power k\(x\y)] in E by BCIALG_1:2
;
hence thesis by Th4;
end;
A17: P[0] by A14,Th1;
for n holds P[n] from NAT_1:sch 2(A17,A16);
hence thesis;
end;
E is_symmetric_in field E by RELAT_2:def 11;
then
E is_transitive_in field E & [((x,(x\y))to_power i,y\x)to_power j,y
] in E by A7,A8,A15,RELAT_2:def 3,def 16;
hence thesis by A8,A11,RELAT_2:def 8;
end;
hence [x,y] in E iff x\y in I & y\x in I by A2,Th40;
end;
hence thesis by Def12;
end;
theorem
IConSet(X) c= ConSet(X)
proof
let x be object;
assume x in IConSet(X);
then ex I being Ideal of X st x is I-congruence of X,I by Def13;
hence thesis;
end;
theorem Th45:
ConSet(X) c= LConSet(X)
proof
let x be object;
assume x in ConSet(X);
then ex R being Congruence of X st x=R;
then x is L-congruence of X by Th36;
hence thesis;
end;
theorem Th46:
ConSet(X) c= RConSet(X)
proof
let x be object;
assume x in ConSet(X);
then ex R being Congruence of X st x=R;
then x is R-congruence of X by Th36;
hence thesis;
end;
theorem
ConSet(X) = LConSet(X)/\RConSet(X)
proof
ConSet(X) c= LConSet(X) & ConSet(X) c= RConSet(X) by Th45,Th46;
hence ConSet(X) c= LConSet(X)/\RConSet(X) by XBOOLE_1:19;
thus LConSet(X)/\RConSet(X) c= ConSet(X)
proof
let x be object;
assume
A1: x in LConSet(X)/\RConSet(X);
then x in RConSet(X) by XBOOLE_0:def 4;
then
A2: ex R being R-congruence of X st x=R;
x in LConSet(X) by A1,XBOOLE_0:def 4;
then ex L being L-congruence of X st x=L;
then x is Congruence of X by A2,Th36;
hence thesis;
end;
end;
theorem
(for LC holds LC is I-congruence of X,I) implies E = RI
proof
assume
A1: for LC holds LC is I-congruence of X,I;
let x1,y1 be object;
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
proof
assume
A3: [x1,y1] in E;
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,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 thesis by A4,A6,Def12;
end;
thus [x1,y1] in RI implies [x1,y1] in E
proof
assume
A7: [x1,y1] in RI;
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,y as Element of X by A9;
x\y in I & y\x in I by A7,A8,Def12;
hence thesis by A2,A8,Def12;
end;
end;
theorem
(for RC holds RC is I-congruence of X,I) implies E = RI
proof
assume
A1: for RC holds RC is I-congruence of X,I;
let x1,y1 be object;
E is R-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
proof
assume
A3: [x1,y1] in E;
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,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 thesis by A4,A6,Def12;
end;
thus [x1,y1] in RI implies [x1,y1] in E
proof
assume
A7: [x1,y1] in RI;
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,y as Element of X by A9;
x\y in I & y\x in I by A7,A8,Def12;
hence thesis by A2,A8,Def12;
end;
end;
theorem
Class(LC,0.X) is closed Ideal of X
proof
A1: now
let x,y be Element of X;
assume that
A2: x\y in Class(LC,0.X) and
A3: y in Class(LC,0.X);
[0.X,y] in LC by A3,EQREL_1:18;
then [x\0.X,x\y] in LC by Def10;
then [x,x\y] in LC by BCIALG_1:2;
then
A4: [x\y,x] in LC by EQREL_1:6;
[0.X,x\y] in LC by A2,EQREL_1:18;
then [0.X,x] in LC by A4,EQREL_1:7;
hence x in Class(LC,0.X)by EQREL_1:18;
end;
[0.X,0.X] in LC by EQREL_1:5;
then 0.X in Class(LC,0.X) by EQREL_1:18;
then reconsider Rx=Class(LC,0.X) as Ideal of X by A1,BCIALG_1:def 18;
now
let x be Element of Rx;
[0.X,x] in LC by EQREL_1:18;
then [(0.X)`,x`] in LC by Def10;
then [0.X,x`] in LC by BCIALG_1:def 5;
hence x` in Class(LC,0.X) by EQREL_1:18;
end;
hence thesis by BCIALG_1:def 19;
end;
:: Quotient Algebras
reserve E for Congruence of X;
reserve RI for I-congruence of X,I;
registration
let X,E;
cluster Class E -> non empty;
coherence
proof
Class(E,0.X) in Class E by EQREL_1:def 3;
hence thesis;
end;
end;
definition
let X,E;
func EqClaOp E -> BinOp of Class E means
:Def17:
for W1,W2 being Element of
Class(E) for x,y st W1=Class(E,x) & W2=Class(E,y) holds it.(W1,W2)=Class(E,x\y)
;
existence
proof
defpred P[Element of Class E,Element of Class E,set] means for x,y st $1 =
Class(E,x) & $2 = Class(E,y) holds $3 = Class(E,x\y);
A1: for W1,W2 being Element of Class E ex V being Element of Class E st P[
W1,W2,V]
proof
let W1,W2 be Element of Class E;
consider x1 being object such that
A2: x1 in the carrier of X and
A3: W1 = Class(E,x1) by EQREL_1:def 3;
consider y1 being object such that
A4: y1 in the carrier of X and
A5: W2 = Class(E,y1) by EQREL_1:def 3;
reconsider x1,y1 as Element of X by A2,A4;
reconsider C = Class(E,x1\y1) as Element of Class E by EQREL_1:def 3;
take C;
now
let x,y;
assume that
A6: W1=Class(E,x) and
A7: W2=Class(E,y);
y in Class(E,y1) by A5,A7,EQREL_1:23;
then
A8: [y1,y] in E by EQREL_1:18;
x in Class(E,x1) by A3,A6,EQREL_1:23;
then [x1,x] in E by EQREL_1:18;
then [x1\y1,x\y] in E by A8,Def9;
then x\y in Class(E,x1\y1) by EQREL_1:18;
hence C = Class(E,x\y) by EQREL_1:23;
end;
hence thesis;
end;
thus ex B being BinOp of Class E st for W1,W2 being Element of Class E
holds P[W1,W2,B.(W1,W2)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof
let o1,o2 be BinOp of Class E;
assume
A9: for W1,W2 being Element of Class E for x,y st W1=Class(E,x)&W2=
Class(E,y)holds o1.(W1,W2)=Class(E,x\y);
assume
A10: for W1,W2 being Element of Class E for x,y st W1=Class(E,x)&W2=
Class(E,y)holds o2.(W1,W2)=Class(E,x\y);
now
let W1,W2 be Element of Class(E);
consider x being object such that
A11: x in the carrier of X and
A12: W1 = Class(E,x) by EQREL_1:def 3;
consider y being object such that
A13: y in the carrier of X and
A14: W2 = Class(E,y) by EQREL_1:def 3;
reconsider x,y as Element of X by A11,A13;
o1.(W1,W2)=Class(E,x\y) by A9,A12,A14;
hence o1.(W1,W2) = o2.(W1,W2) by A10,A12,A14;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let X,E;
func zeroEqC(E) -> Element of Class E equals
Class(E,0.X);
coherence by EQREL_1:def 3;
end;
::Quotient Algebras
definition
let X,E;
func X./.E -> BCIStr_0 equals
BCIStr_0(#Class E,EqClaOp E,zeroEqC(E)#);
coherence;
end;
registration
let X;
let E be Congruence of X;
cluster X./.E -> non empty;
coherence;
end;
reserve W1,W2 for Element of Class E;
definition
let X,E,W1,W2;
func W1\W2 -> Element of Class E equals
(EqClaOp E).(W1,W2);
coherence;
end;
theorem Th51:
X./.RI is BCI-algebra
proof
reconsider IT = X./.RI as non empty BCIStr_0;
A1: now
let w1,w2,w3 be Element of 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,y1,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;
end;
A10: now
let w1,w2,w3 be Element of 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,y1,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;
end;
A18: now
let w1,w2 be Element of IT;
assume that
A19: w1\w2=0.IT and
A20: w2\w1=0.IT;
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,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;
end;
now
let w1 be Element of IT;
w1 in the carrier of IT;
then consider x1 being object such that
A26: x1 in the carrier of X and
A27: w1 = Class(RI,x1) by EQREL_1:def 3;
reconsider x1 as Element of X by A26;
w1\w1=Class(RI,x1\x1) by A27,Def17;
hence w1\w1 = 0.IT by BCIALG_1:def 5;
end;
hence thesis by A1,A10,A18,BCIALG_1:def 3,def 4,def 5,def 7;
end;
registration
let X,I,RI;
cluster X./.RI -> strict being_B being_C being_I being_BCI-4;
coherence by Th51;
end;
theorem
for X,I st I = BCK-part(X) holds for RI being I-congruence of X,I
holds X./.RI is p-Semisimple BCI-algebra
proof
let X,I;
assume
A1: I = BCK-part(X);
let RI be I-congruence of X,I;
set IT = X./.RI;
for w1 being Element of IT holds (w1`)` = w1
proof
let w1 be Element of 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;
reconsider x1 as Element of X by A2;
w1`= Class(RI,x1`) by A3,Def17;
then
A4: w1``=Class(RI,x1``) by Def17;
x1\((x1`)`) is positive Element of X by Th28;
then 0.X <= x1\(x1``) by Def2;
then
A5: x1\(x1``) in I by A1;
0.X in I by BCIALG_1:def 18;
then (x1`)`\x1 in I by BCIALG_1:1;
then [x1``,x1] in RI by A5,Def12;
hence thesis by A3,A4,EQREL_1:35;
end;
hence thesis by BCIALG_1:54;
end;