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