theorem Th81: :: ZF_LANG:81

for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)}