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