consider a being Element of A;
consider f being V2() ManySortedSet of A;
take f ; :: thesis: not f is empty-yielding
take a ; :: according to PBOOLE:def 15 :: thesis: ( a in A & not f . a is empty )
thus ( a in A & not f . a is empty ) ; :: thesis: verum