let I be non empty set ; :: thesis: for X, Y being ManySortedSet of I st X /\ Y = [[0]] I holds
not X overlaps Y
let X, Y be ManySortedSet of I; :: thesis: ( X /\ Y = [[0]] I implies not X overlaps Y )
assume A1: X /\ Y = [[0]] I ; :: thesis: not X overlaps Y
assume X overlaps Y ; :: thesis: contradiction
then consider x being ManySortedSet of I 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