theorem Th130: :: ZF_LANG1:130

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