take ExtNAT ; :: thesis: for b₁ being ExtNat holds b₁ in ExtNAT
thus for b₁ being ExtNat holds b₁ in ExtNAT by Def1; :: thesis: verum