let I be set ; :: thesis: for X being ManySortedSet of I st X <> EmptyMS I holds
X meets X
let X be ManySortedSet of I; :: thesis: ( X <> EmptyMS I implies X meets X )
X = X (/\) X ;
hence ( X <> EmptyMS I implies X meets X ) by Th111; :: thesis: verum