let I be set ; :: thesis: for X being ManySortedSet of holds
( X is empty-yielding iff X = [0] I )
let X be ManySortedSet of ; :: 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