theorem :: ZF_LANG:28

for H being ZF-formula st H . 1 = 4 holds
H is universal by Th23;