let I be non empty set ; :: thesis: for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds
not X overlaps Y
let X, Y be ManySortedSet of I; :: thesis: ( X (/\) Y = EmptyMS I implies not X overlaps Y )
assume A1: X (/\) Y = EmptyMS 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, Th124; :: thesis: verum