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