let S be locally_directed OrderSortedSign; 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; 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; 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; 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; ( 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 ( [x,y] in E . s implies OSClass (E,x) = OSClass (E,y) )
assume
OSClass (
E,
x)
= OSClass (
E,
y)
;
[x,y] in E . sthen
[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;
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
; 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; verum