theorem Th5: :: BSPACE:5

0. Z_2 = 0 by NAT_1:44, SUBSET_1:def 8;