[Agda] How to formalize 'there exists a set' phrase?

[Benja Fallenstein]

2010/7/7 Andreas Abel <andreas.abel at ifi.lmu.de>:
>
> On Jul 7, 2010, at 4:34 PM, Vag Vagoff wrote:
>>
>> Okay. But it is still unknown how to state "There exist a subset of A that
>> property P holds" (i.e. "there exist a set of primes")
>
> P is that very subset.

Oh, I thought what was meant was "there exists a subset S of A such
that S fulfills property P," but I guess that Andreas' reading ("there
exists a subset S of A such that all x in A: x is in S iff x fulfills
P") is what was meant. Sorry if I added to the confusion!

All the best,
- Benja