let I be non empty set ; :: thesis: for x, X, Y being ManySortedSet of st x in X & x in Y holds
X /\ Y <> [0] I
let x, X, Y be ManySortedSet of ; :: 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