set i = the Element of I;
let M be ManySortedSet of I; :: thesis: ( M is V8() implies not M is V9() )
assume A1: M is V8() ; :: thesis: M is V9()
take the Element of I ; :: according to PBOOLE:def 12 :: thesis: ( the Element of I in I & not M . the Element of I is empty )
thus the Element of I in I ; :: thesis: not M . the Element of I is empty
thus not M . the Element of I is empty by A1; :: thesis: verum