theorem Th77: :: ZF_LANG:77

for x, y being Variable
for H being ZF-formula holds
( H is_subformula_of x 'in' y iff H = x 'in' y )