let S be locally_directed OrderSortedSign; :: thesis: for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass E,x = OSClass E,y iff [x,y] in E . s )
let U1 be non-empty OSAlgebra of S; :: thesis: for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass E,x = OSClass E,y iff [x,y] in E . s )
let E be MSEquivalence-like OrderSortedRelation of U1; :: thesis: for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass E,x = OSClass E,y iff [x,y] in E . s )
let s be Element of S; :: thesis: for x, y being Element of the Sorts of U1 . s holds
( OSClass E,x = OSClass E,y iff [x,y] in E . s )
let x, y be Element of the Sorts of U1 . s; :: thesis: ( OSClass E,x = OSClass E,y iff [x,y] in E . s )
reconsider SU = the Sorts of U1 as OrderSortedSet of by OSALG_1:17;
A1: x in the Sorts of U1 -carrier_of (CComp s) by Th6;
A2: s in CComp s by EQREL_1:28;
A3: E is os-compatible by Def3;

hereby :: thesis: ( [x,y] in E . s implies OSClass E,x = OSClass E,y )

assume OSClass E,x = OSClass E,y ; :: thesis: [x,y] in E . s
then [x,y] in CompClass E,(CComp s) by A1, EQREL_1:44;
then consider s1 being Element of S such that
A4: ( s1 in CComp s & [x,y] in E . s1 ) by Def11;
reconsider sn1 = s, s11 = s1 as Element of S ;
A5: ( x in SU . s11 & y in SU . s11 ) by A4, ZFMISC_1:106;
consider s2 being Element of S such that
A6: ( s2 in CComp s & s11 <= s2 & sn1 <= s2 ) by A2, A4, WAYBEL_0:def 1;
[x,y] in E . s2 by A3, A4, A5, A6, Def1;
hence [x,y] in E . s by A3, A6, Def1; :: thesis: verum

end;

assume A7: [x,y] in E . s ; :: thesis: OSClass E,x = OSClass E,y
A8: x in the Sorts of U1 -carrier_of (CComp s) by Th6;
s in CComp s by EQREL_1:28;
then [x,y] in CompClass E,(CComp s) by A7, Def11;
hence OSClass E,x = OSClass E,y by A8, EQREL_1:44; :: thesis: verum