theorem Th135: :: ZF_LANG1:135

for x being Variable holds
( x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )