let I be set ; :: thesis: for X being ManySortedSet of I holds X (\+\) (EmptyMS I) = X
let X be ManySortedSet of I; :: thesis: X (\+\) (EmptyMS I) = X
thus X (\+\) (EmptyMS I) = X (\/) ((EmptyMS I) (\) X) by Th59
.= X (\/) (EmptyMS I) by Th60
.= X by Th22, Th43 ; :: thesis: verum