theorem Th137: :: ZF_LANG1:137

for H being ZF-formula
for a being set st a in variables_in H holds
( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )