theorem Th136: :: ZF_LANG1:136

for x being Variable holds not x in {0,1,2,3,4}