let S be non empty set ; :: thesis: for A being non-empty ManySortedSet of S
for R being ManySortedRelation of A
for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds
for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
let A be non-empty ManySortedSet of S; :: thesis: for R being ManySortedRelation of A
for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds
for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
let R be ManySortedRelation of A; :: thesis: for E being MSEquivalence_Relation-like ManySortedRelation of A st R c= E holds
for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
let E be MSEquivalence_Relation-like ManySortedRelation of A; :: thesis: ( R c= E implies for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s )
assume A1: R c= E ; :: thesis: for s being Element of S
for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
let s be Element of S; :: thesis: for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s
A2: E . s is Equivalence_Relation of (A . s) by MSUALG_4:def 2;
R . s c= E . s by A1;
hence for a, b being Element of A . s st a,b are_convertible_wrt R . s holds
[a,b] in E . s by A2, Th40; :: thesis: verum