let I be non empty set ; :: thesis: for M being ManySortedSet of I
for x being Element of I st not x in supp M holds
M . x = {}
let M be ManySortedSet of I; :: thesis: for x being Element of I st not x in supp M holds
M . x = {}
let x be Element of I; :: thesis: ( not x in supp M implies M . x = {} )
assume not x in supp M ; :: thesis: M . x = {}
then not x in { v where v is Element of I : M . v <> {} } by Def3;
hence M . x = {} ; :: thesis: verum