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

hereby :: thesis: ( X = EmptyMS I implies X is empty-yielding )

assume X is empty-yielding ; :: thesis: X = EmptyMS I
then for i being object st i in I holds
X . i = {} ;
hence X = EmptyMS I by Th6; :: thesis: verum

end;

assume A1: X = EmptyMS I ; :: thesis: X is empty-yielding
let i be object ; :: according to PBOOLE:def 12 :: 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; :: thesis: verum