theorem Th95: :: ZF_LANG1:95

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