let I be set ; :: thesis: for X being ManySortedSet of I holds
( X is empty-yielding iff X = [[0]] I )
let X be ManySortedSet of I; :: thesis: ( X is empty-yielding iff X = [[0]] I )

hereby :: thesis: ( X = [[0]] I implies X is empty-yielding )

assume X is empty-yielding ; :: thesis: X = [[0]] I
then for i being set st i in I holds
X . i = {} by Def15;
hence X = [[0]] I by Th6; :: thesis: verum

end;

assume A1: X = [[0]] I ; :: thesis: X is empty-yielding
let i be set ; :: according to PBOOLE:def 15 :: thesis: ( i in I implies X . i is empty )
assume i in I ; :: thesis: X . i is empty
thus X . i is empty by A1, Th5; :: thesis: verum