let O1, O2 be strict RelStr ; :: thesis: ( the carrier of O1 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) & the carrier of O2 = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) implies O1 = O2 )

assume that
A5: the carrier of O1 = Class () and
A6: for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of O1 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) and
A7: the carrier of O2 = Class () and
A8: for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of O2 iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),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 ()) by A5;
reconsider I2 = the InternalRel of O2 as Relation of (Class ()) by A7;
for X, Y being Element of Class () holds
( [X,Y] in I1 iff [X,Y] in I2 )
proof
let X, Y be Element of Class (); :: 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 ((),x) & Y = Class ((),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 ; :: thesis: verum