let I be non empty set ; :: thesis: for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X /\ Y <> [[0]] I
let x, X, Y be ManySortedSet of I; :: thesis: ( x in X & x in Y implies X /\ Y <> [[0]] I )
assume ( x in X & x in Y ) ; :: thesis: X /\ Y <> [[0]] I
then x in X /\ Y by Th8;
hence X /\ Y <> [[0]] I by Th136; :: thesis: verum