let x be set ; :: according to MEMBERED:def 6 :: thesis: ( not x in the carrier of dL-Z_2 or x is natural )
thus ( not x in the carrier of dL-Z_2 or x is natural ) by CARD_1:50, TARSKI:def 2; :: thesis: verum