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 )
proof
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;
then A10: I1 = I2 by RELSET_1:def 2;
reconsider rel = the InternalRel of O2 as Relation of the carrier of O1 by A9;
thus O1 = O2 by A9, A10; :: thesis: verum