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

hereby :: thesis: ( X = EmptyMS I implies X is V9() )

assume X is V9() ; :: 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 V9()
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, Th5; :: thesis: verum