let I be set ; :: thesis: for X being ManySortedSet of I st X c= EmptyMS I holds
X = EmptyMS I
let X be ManySortedSet of I; :: thesis: ( X c= EmptyMS I implies X = EmptyMS I )
assume X c= EmptyMS I ; :: thesis: X = EmptyMS I
then ( X c= EmptyMS I & EmptyMS I c= X ) by Th43;
hence X = EmptyMS I by Lm1; :: thesis: verum