take the V8() ManySortedSet of A ; :: thesis: the V8() ManySortedSet of A is V9()
take the Element of A ; :: according to PBOOLE:def 12 :: thesis: ( the Element of A in A & not the V8() ManySortedSet of A . the Element of A is empty )
thus ( the Element of A in A & not the V8() ManySortedSet of A . the Element of A is empty ) ; :: thesis: verum