reconsider z = 0 as Element of dL-Z_2 by CARD_1:50, TARSKI:def 2;
take z ; :: thesis: z is empty
thus z is empty ; :: thesis: verum