let O1, O2 be strict RelStr ; ( 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 ) )
; 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 )
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; verum