theorem Th17: :: ZF_LANG:17

for x being Variable
for H being ZF-formula holds (All (x,H)) . 1 = 4