let f be Function; :: thesis: ( f is SetPrimes -defined implies f is NAT -defined )
assume f is SetPrimes -defined ; :: thesis: f is NAT -defined
then A1: dom f c= SetPrimes by RELAT_1:def 18;
SetPrimes c= NAT ;
hence dom f c= NAT by A1; :: according to RELAT_1:def 18 :: thesis: verum