thus dL-Z_2 is strict ; :: thesis: ( not dL-Z_2 is empty & not dL-Z_2 is degenerated )
thus not the carrier of dL-Z_2 is empty ; :: according to STRUCT_0:def 1 :: thesis: not dL-Z_2 is degenerated
0 in 2 by CARD_1:50, TARSKI:def 2;
then A1: 0. dL-Z_2 = 0 by SUBSET_1:def 8;
1 in 2 by CARD_1:50, TARSKI:def 2;
hence 0. dL-Z_2 <> 1. dL-Z_2 by A1, SUBSET_1:def 8; :: according to STRUCT_0:def 8 :: thesis: verum