theorem Th157: :: ZF_LANG1:157

for H being ZF-formula
for x, y being Variable holds H / (x,y) in WFF