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