let S be non empty set ; :: thesis: for A being non-empty 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 non-empty ManySortedSet of S; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: E is MSEquivalence_Relation-like
let i be object ; :: according to MSUALG_4:def 2 :: thesis: for b₁ being Element of bool [:(A . i),(A . i):] holds
( not i in S or not E . i = b₁ or b₁ is Element of bool [:(A . i),(A . i):] )
let P be Relation of (A . i); :: thesis: ( not i in S or not E . i = P or P is Element of bool [:(A . i),(A . i):] )
assume i in S ; :: thesis: ( 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; :: thesis: verum