theorem Th51: :: ZF_LANG:51

for x, y being Variable
for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y