theorem :: ZF_LANG:27

for H being ZF-formula st H . 1 = 3 holds
H is conjunctive by Th23;