theorem Th128: :: ZF_LANG1:128

for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))