sorry to bother again :(

Dear All,

Sorry to bother again with some details. I have the following introduction and question.

Let A be the following set (it is not exactly the Mizar syntax:)):

::starts here

    defpred P[Element of NAT,Element of NAT] means ...

    setA = {[a,b] where a is Element of NAT, b is Element of NAT: P[a,b]}

   theorem setA is non empty
   proof
     ex a,b being Element of NAT st [a,b] in setA 
     proof
        take 1 , 2 ;
        P[1,2] proof ... end;
        hence [1,2] in setA;
::>                                #4  
     end;
     then consider a,b being Element of NAT such that L1: [a,b] in setA;
     thus thesis by L1;  ::BOOLE is in the requirements
  end;

::ends here


After proving that property P holds for particular objects (1 and 2 in this case), that is, P[1,2]; 
what other conditions Mizar expects for the "[1,2] in setA" to hold?

I have found the solution for finite sets in the ENUMSET1.miz article  but not for this case where 
set's elements are those that satisfy a property. 

Thank you again and sorry my troubles...

Adem Ozyavas
Texas Tech University