theorem Counter0: :: MOEBIUS3:2

for Z being Subset of REAL st not 0 in Z holds
(id Z) " {0} = {}