let x be set ; :: thesis: ( x is Element of <NAT,+,0> iff x is Element of NAT )
H₁( <NAT,+,0> ) = H₁( <NAT,+> ) by Th18
.= NAT by Def27 ;
hence ( x is Element of <NAT,+,0> iff x is Element of NAT ) ; :: thesis: verum