theorem Th174: :: ZF_LANG1:174

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