let S be non empty set ; :: thesis: for A being non-empty ManySortedSet of S
for R being ManySortedRelation of A
for s being Element of S
for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )
let A be non-empty ManySortedSet of S; :: thesis: for R being ManySortedRelation of A
for s being Element of S
for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )
let R be ManySortedRelation of A; :: thesis: for s being Element of S
for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )
let s be Element of S; :: thesis: for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s )
(EqCl R) . s = EqCl (R . s) by MSUALG_5:def 3;
hence for a, b being Element of A . s holds
( [a,b] in (EqCl R) . s iff a,b are_convertible_wrt R . s ) by Th41; :: thesis: verum