let I be non empty set ; :: thesis: for X, Y being ManySortedSet of st X /\ Y = [0] I holds
X does_not_overlap Y
let X, Y be ManySortedSet of ; :: thesis: ( X /\ Y = [0] I implies X does_not_overlap Y )
assume A1: X /\ Y = [0] I ; :: thesis: X does_not_overlap Y
assume X overlaps Y ; :: thesis: contradiction
then consider x being ManySortedSet of such that
A2: ( x in X & x in Y ) by Th11;
x in X /\ Y by A2, Th8;
hence contradiction by A1, Th136; :: thesis: verum