let I be non empty set ; :: thesis: for x being ManySortedSet of I holds not x in EmptyMS I
set i = the Element of I;
given x being ManySortedSet of I such that A1: x in EmptyMS I ; :: thesis: contradiction
x . the Element of I in (EmptyMS I) . the Element of I by A1;
hence contradiction ; :: thesis: verum