let O1, O2 be strict RelStr ; :: thesis: ( the carrier of O1 = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) & the carrier of O2 = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) implies O1 = O2 )

assume that

A5: the carrier of O1 = Class (EqRelOf A) and

A6: for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) and

A7: the carrier of O2 = Class (EqRelOf A) and

A8: for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ; :: thesis: O1 = O2

A9: the carrier of O1 = the carrier of O2 by A5, A7;

reconsider I1 = the InternalRel of O1 as Relation of (Class (EqRelOf A)) by A5;

reconsider I2 = the InternalRel of O2 as Relation of (Class (EqRelOf A)) by A7;

for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in I1 iff [X,Y] in I2 )

reconsider rel = the InternalRel of O2 as Relation of the carrier of O1 by A9;

thus O1 = O2 by A9, A10; :: thesis: verum

( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) & the carrier of O2 = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) implies O1 = O2 )

assume that

A5: the carrier of O1 = Class (EqRelOf A) and

A6: for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) and

A7: the carrier of O2 = Class (EqRelOf A) and

A8: for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ; :: thesis: O1 = O2

A9: the carrier of O1 = the carrier of O2 by A5, A7;

reconsider I1 = the InternalRel of O1 as Relation of (Class (EqRelOf A)) by A5;

reconsider I2 = the InternalRel of O2 as Relation of (Class (EqRelOf A)) by A7;

for X, Y being Element of Class (EqRelOf A) holds

( [X,Y] in I1 iff [X,Y] in I2 )

proof

then A10:
I1 = I2
by RELSET_1:def 2;
let X, Y be Element of Class (EqRelOf A); :: thesis: ( [X,Y] in I1 iff [X,Y] in I2 )

( [X,Y] in I1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) by A6;

hence ( [X,Y] in I1 iff [X,Y] in I2 ) by A8; :: thesis: verum

end;( [X,Y] in I1 iff ex x, y being Element of A st

( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) by A6;

hence ( [X,Y] in I1 iff [X,Y] in I2 ) by A8; :: thesis: verum

reconsider rel = the InternalRel of O2 as Relation of the carrier of O1 by A9;

thus O1 = O2 by A9, A10; :: thesis: verum