let S be non empty set ; for A being V2() ManySortedSet of S
for R, E being ManySortedRelation of A st ( for s being Element of S
for a, b being Element of A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds
E is MSEquivalence_Relation-like
let A be V2() ManySortedSet of S; for R, E being ManySortedRelation of A st ( for s being Element of S
for a, b being Element of A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) holds
E is MSEquivalence_Relation-like
let R, E be ManySortedRelation of A; ( ( for s being Element of S
for a, b being Element of A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s ) ) implies E is MSEquivalence_Relation-like )
assume A1:
for s being Element of S
for a, b being Element of A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s )
; E is MSEquivalence_Relation-like
let i be set ; MSUALG_4:def 2 for b1 being Element of bool [:(A . i),(A . i):] holds
( not i in S or not E . i = b1 or b1 is Element of bool [:(A . i),(A . i):] )
let P be Relation of (A . i); ( not i in S or not E . i = P or P is Element of bool [:(A . i),(A . i):] )
assume
i in S
; ( not E . i = P or P is Element of bool [:(A . i),(A . i):] )
then reconsider s = i as Element of S ;
for a, b being set st a in A . s & b in A . s holds
( [a,b] in E . s iff a,b are_convertible_wrt R . s )
by A1;
hence
( not E . i = P or P is Element of bool [:(A . i),(A . i):] )
by Th39; verum