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