take the natural number ; :: thesis: the natural number is ext-natural
thus the natural number is ext-natural ; :: thesis: verum