let X be set ; :: thesis:

hereby :: thesis:

assume A1: X is ext-natural-membered ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in X ; :: thesis:
then x is ext-natural by A1;
hence x in ExtNAT ; :: thesis:

end;

hence X c= ExtNAT by TARSKI:def 3; :: thesis:

end;

assume X c= ExtNAT ; :: thesis:
hence X is ext-natural-membered ; :: thesis: