theorem :: ZF_LANG1:126

for H being ZF-formula
for x being Variable
for M being non empty set holds M |= (All (x,H)) => H