theorem Th169: :: ZF_LANG1:169

for H being ZF-formula
for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )