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 S by OSALG_1:17;
A1: s in CComp s by EQREL_1:20;
A2: E is os-compatible by Def2;
A3: x in the Sorts of U1 -carrier_of (CComp s) by Th5;

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 A3, EQREL_1:35;
then consider s1 being Element of S such that
A4: s1 in CComp s and
A5: [x,y] in E . s1 by Def9;
reconsider sn1 = s, s11 = s1 as Element of S ;
consider s2 being Element of S such that
s2 in CComp s and
A6: s11 <= s2 and
A7: sn1 <= s2 by A1, A4, WAYBEL_0:def 1;
( x in SU . s11 & y in SU . s11 ) by A5, ZFMISC_1:87;
then [x,y] in E . s2 by A2, A5, A6;
hence [x,y] in E . s by A2, A7; :: thesis: verum

end;

A8: s in CComp s by EQREL_1:20;
A9: x in the Sorts of U1 -carrier_of (CComp s) by Th5;
assume [x,y] in E . s ; :: thesis: OSClass (E,x) = OSClass (E,y)
then [x,y] in CompClass (E,(CComp s)) by A8, Def9;
hence OSClass (E,x) = OSClass (E,y) by A9, EQREL_1:35; :: thesis: verum